COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	 "PROVEALL"
C00106 ENDMK
C⊗;
;;; "PROVEALL"
(PROVEALL
  '((NOTE-LIB "BOOT-STRAP.LIB" "BOOT-STRAP.LISP")
    (PROVE-LEMMA PLUS-RIGHT-ID2 (REWRITE)
		 (IMPLIES (NOT (NUMBERP Y))
			  (EQUAL (PLUS X Y)
				 (FIX X))))
    (PROVE-LEMMA PLUS-ADD1 (REWRITE)
		 (EQUAL (PLUS X (ADD1 Y))
			(IF (NUMBERP Y)
			    (ADD1 (PLUS X Y))
			    (ADD1 X))))
    (PROVE-LEMMA COMMUTATIVITY2-OF-PLUS (REWRITE)
		 (EQUAL (PLUS X (PLUS Y Z))
			(PLUS Y (PLUS X Z)))) 
    (PROVE-LEMMA COMMUTATIVITY-OF-PLUS (REWRITE)
		 (EQUAL (PLUS X Y)
			(PLUS Y X)))
    (PROVE-LEMMA ASSOCIATIVITY-OF-PLUS (REWRITE)
		 (EQUAL (PLUS (PLUS X Y)
			      Z)
			(PLUS X (PLUS Y Z)))) 
    (PROVE-LEMMA PLUS-EQUAL-0 (REWRITE)
		 (EQUAL (EQUAL (PLUS A B)
			       0)
			(AND (ZEROP A)
			     (ZEROP B))))
    (PROVE-LEMMA DIFFERENCE-X-X (REWRITE)
		 (EQUAL (DIFFERENCE X X)  0))
    (PROVE-LEMMA DIFFERENCE-PLUS (REWRITE)
		 (AND (EQUAL (DIFFERENCE (PLUS X Y)
					 X)
			     (FIX Y))
		      (EQUAL (DIFFERENCE (PLUS Y X)
					 X)
			     (FIX Y))))
    (PROVE-LEMMA PLUS-CANCELLATION (REWRITE)
		 (EQUAL (EQUAL (PLUS A B)
			       (PLUS A C))
			(EQUAL (FIX B) (FIX C))))
    (PROVE-LEMMA DIFFERENCE-0 (REWRITE)
		 (IMPLIES (NOT (LESSP Y X))
			  (EQUAL (DIFFERENCE X Y)
				 0)))
    (PROVE-LEMMA EQUAL-DIFFERENCE-0 (REWRITE)
		 (EQUAL (EQUAL 0 (DIFFERENCE X Y))
			(NOT (LESSP Y X))))
    (PROVE-LEMMA DIFFERENCE-CANCELLATION-0 (REWRITE)
		 (EQUAL (EQUAL X (DIFFERENCE X Y))
			(AND (NUMBERP X)
			     (OR (EQUAL X 0)
				 (ZEROP Y)))))
    (PROVE-LEMMA DIFFERENCE-CANCELLATION-1 (REWRITE)
		 (EQUAL (EQUAL (DIFFERENCE X Y)
			       (DIFFERENCE Z Y))
			(IF (LESSP X Y)
			    (NOT (LESSP Y Z))
			    (IF (LESSP Z Y)
				(NOT (LESSP Y X))
				(EQUAL (FIX X)
				       (FIX Z))))))
    (DEFN APPEND (X Y)
      (IF (LISTP X)
	  (CONS (CAR X)
		(APPEND (CDR X)
			Y))
	  Y))
    (DEFN DELETE (X Y)
      (IF (LISTP Y)
	  (IF (EQUAL X (CAR Y))
	      (CDR Y)
	      (CONS (CAR Y)
		    (DELETE X (CDR Y))))
	  Y))
    (DEFN SUBBAGP (X Y)
      (IF (LISTP X)
	  (IF (MEMBER (CAR X)
		      Y)
	      (SUBBAGP (CDR X)
		       (DELETE (CAR X)
			       Y))
	      F)
	  T))
    (DEFN BAGDIFF (X Y)
      (IF (LISTP Y)
	  (IF (MEMBER (CAR Y)
		      X)
	      (BAGDIFF (DELETE (CAR Y)
			       X)
		       (CDR Y))
	      (BAGDIFF X (CDR Y)))
	  X))
    (DEFN BAGINT (X Y)
      (IF (LISTP X)
	  (IF (MEMBER (CAR X)
		      Y)
	      (CONS (CAR X)
		    (BAGINT (CDR X)
			    (DELETE (CAR X)
				    Y)))
	      (BAGINT (CDR X)
		      Y))
	  NIL))
    (PROVE-LEMMA DELETE-NON-MEMBER (REWRITE)
		 (IMPLIES (NOT (MEMBER X Y))
			  (EQUAL (DELETE X Y)
				 Y)))
    (PROVE-LEMMA MEMBER-DELETE (REWRITE)
		 (IMPLIES (MEMBER X (DELETE U V))
			  (MEMBER X V)))
    (PROVE-LEMMA COMMUTATIVITY-OF-DELETE (REWRITE)
		 (EQUAL (DELETE X (DELETE Y Z))
			(DELETE Y (DELETE X Z))))
    (PROVE-LEMMA SUBBAGP-DELETE (REWRITE)
		 (IMPLIES (SUBBAGP X (DELETE U Y))
			  (SUBBAGP X Y)))
    (PROVE-LEMMA SUBBAGP-CDR1 (REWRITE)
		 (IMPLIES (SUBBAGP X Y)
			  (SUBBAGP (CDR X)
				   Y)))
    (PROVE-LEMMA SUBBAGP-CDR2 (REWRITE)
		 (IMPLIES (SUBBAGP X (CDR Y))
			  (SUBBAGP X Y)))
    (PROVE-LEMMA SUBBAGP-BAGINT1 (REWRITE)
		 (SUBBAGP (BAGINT X Y)
			  X))
    (PROVE-LEMMA SUBBAGP-BAGINT2 (REWRITE)
		 (SUBBAGP (BAGINT X Y)
			  Y))
    (DEFN PLUS-FRINGE (X)
      (IF (AND (LISTP X)
	       (EQUAL (CAR X)
		      (QUOTE PLUS)))
	  (APPEND (PLUS-FRINGE (CADR X))
		  (PLUS-FRINGE (CADDR X)))
	  (CONS X NIL)))
    (DEFN PLUS-TREE (L)
      (IF (NLISTP L)
	  (QUOTE (QUOTE 0))
	  (IF (NLISTP (CDR L))
	      (LIST (QUOTE FIX)
		    (CAR L))
	      (IF (NLISTP (CDDR L))
		  (LIST (QUOTE PLUS)
			(CAR L)
			(CADR L))
		  (LIST (QUOTE PLUS)
			(CAR L)
			(PLUS-TREE (CDR L)))))))
    (DEFN
      CANCEL
      (X)
      (IF
	(AND (LISTP X)
	     (EQUAL (CAR X)
		    (QUOTE EQUAL)))
	(IF
	  (AND (LISTP (CADR X))
	       (EQUAL (CAADR X)
		      (QUOTE PLUS))
	       (LISTP (CADDR X))
	       (EQUAL (CAADDR X)
		      (QUOTE PLUS)))
	  (LIST (QUOTE EQUAL)
		(PLUS-TREE (BAGDIFF
			     (PLUS-FRINGE (CADR X))
			     (BAGINT (PLUS-FRINGE (CADR X))
				     (PLUS-FRINGE (CADDR X)))))
		(PLUS-TREE (BAGDIFF
			     (PLUS-FRINGE (CADDR X))
			     (BAGINT (PLUS-FRINGE (CADR X))
				     (PLUS-FRINGE (CADDR X))))))
	  (IF
	    (AND (LISTP (CADR X))
		 (EQUAL (CAADR X)
			(QUOTE PLUS))
		 (MEMBER (CADDR X)
			 (PLUS-FRINGE (CADR X))))
	    (LIST (QUOTE IF)
		  (LIST (QUOTE NUMBERP)
			(CADDR X))
		  (LIST (QUOTE EQUAL)
			(PLUS-TREE (DELETE
				     (CADDR X)
				     (PLUS-FRINGE (CADR X))))
			(QUOTE (QUOTE 0)))
		  (LIST (QUOTE QUOTE)
			F))
	    (IF
	      (AND (LISTP (CADDR X))
		   (EQUAL (CAADDR X)
			  (QUOTE PLUS))
		   (MEMBER (CADR X)
			   (PLUS-FRINGE (CADDR X))))
	      (LIST (QUOTE IF)
		    (LIST (QUOTE NUMBERP)
			  (CADR X))
		    (LIST (QUOTE EQUAL)
			  (QUOTE (QUOTE 0))
			  (PLUS-TREE
			    (DELETE (CADR X)
				    (PLUS-FRINGE (CADDR X)))))
		    (LIST (QUOTE QUOTE)
			  F))
	      X)))
	X))
    (PROVE-LEMMA FORM-LSTP-APPEND (REWRITE)
		 (IMPLIES (AND (FORM-LSTP A)
			       (FORM-LSTP B))
			  (FORM-LSTP (APPEND A B))))
    (PROVE-LEMMA FORM-LSTP-PLUS-FRINGE (REWRITE)
		 (IMPLIES (FORMP X)
			  (FORM-LSTP (PLUS-FRINGE X))))
    (PROVE-LEMMA FORM-LSTP-DELETE (REWRITE)
		 (IMPLIES (FORM-LSTP X)
			  (FORM-LSTP (DELETE Y X))))
    (PROVE-LEMMA FORM-LSTP-BAGDIFF (REWRITE)
		 (IMPLIES (FORM-LSTP X)
			  (FORM-LSTP (BAGDIFF X Y))))
    (PROVE-LEMMA FORMP-PLUS-TREE (REWRITE)
		 (IMPLIES (FORM-LSTP X)
			  (FORMP (PLUS-TREE X))))
    (PROVE-LEMMA NUMBERP-MEANING-PLUS (REWRITE)
		 (IMPLIES (AND (LISTP X)
			       (EQUAL (CAR X)
				      (QUOTE PLUS)))
			  (NUMBERP (MEANING X A))))
    (PROVE-LEMMA NUMBERP-MEANING-PLUS-TREE (REWRITE)
		 (NUMBERP (MEANING (PLUS-TREE L)
				   A)))
    (PROVE-LEMMA MEMBER-IMPLIES-PLUS-TREE-GREATEREQP (REWRITE)
		 (IMPLIES (MEMBER X Y)
			  (NOT (LESSP (MEANING (PLUS-TREE Y)
					       A)
				      (MEANING X A)))))
    (PROVE-LEMMA PLUS-TREE-DELETE (REWRITE)
		 (EQUAL (MEANING (PLUS-TREE (DELETE X Y))
				 A)
			(IF (MEMBER X Y)
			    (DIFFERENCE (MEANING (PLUS-TREE Y)
						 A)
					(MEANING X A))
			    (MEANING (PLUS-TREE Y)
				     A))))
    (PROVE-LEMMA SUBBAGP-IMPLIES-PLUS-TREE-GREATEREQP (REWRITE)
		 (IMPLIES (SUBBAGP X Y)
			  (NOT (LESSP (MEANING (PLUS-TREE Y)
					       A)
				      (MEANING (PLUS-TREE X)
					       A)))))
    (PROVE-LEMMA PLUS-TREE-BAGDIFF (REWRITE)
		 (IMPLIES (SUBBAGP X Y)
			  (EQUAL (MEANING
				   (PLUS-TREE (BAGDIFF Y X))
				   A)
				 (DIFFERENCE
				   (MEANING (PLUS-TREE Y)
					    A)
				   (MEANING (PLUS-TREE X)
					    A)))))
    (PROVE-LEMMA NUMBERP-MEANING-BRIDGE (REWRITE)
		 (IMPLIES (EQUAL (MEANING Z A)
				 (MEANING (PLUS-TREE X)
					  A))
			  (NUMBERP (MEANING Z A))))
    (PROVE-LEMMA
      BRIDGE-TO-SUBBAGP-IMPLIES-PLUS-TREE-GREATEREQP
      (REWRITE)
      (IMPLIES (AND (SUBBAGP Y (PLUS-FRINGE Z))
		    (EQUAL (MEANING Z A)
			   (MEANING (PLUS-TREE (PLUS-FRINGE Z))
				    A)))
	       (EQUAL (LESSP (MEANING Z A)
			     (MEANING (PLUS-TREE Y)
				      A))
		      F))

;   These bridge lemmas are needed because we are soon to prove that MEANING of
;   (PLUS-TREE (PLUS-FRINGE X)) is MEANING of X.  Thus, such facts that the
;   MEANING of the PLUS-TREE of the PLUS-FRINGE is greater than or equal to
;   that of the intersection -- which follows from
;   SUBGAGP-IMPLIES-PLUS-TREE-GREATEREQP -- get covered up.  You will note that
;   in a hand proof of the CANCEL lemma, we do all the arithmetic and such with
;   the PLUS-TREE of the PLUS-FRINGE, and only at the very end rewrite that to
;   the original arg.
 
     )
    (PROVE-LEMMA MEANING-PLUS-TREE-APPEND (REWRITE)
		 (EQUAL (MEANING (PLUS-TREE (APPEND X Y))
				 A)
			(PLUS (MEANING (PLUS-TREE X)
				       A)
			      (MEANING (PLUS-TREE Y)
				       A))))
    (PROVE-LEMMA PLUS-TREE-PLUS-FRINGE (REWRITE)
		 (EQUAL (MEANING (PLUS-TREE (PLUS-FRINGE X))
				 A)
			(FIX (MEANING X A))))
    (PROVE-LEMMA MEMBER-IMPLIES-NUMBERP (REWRITE)
		 (IMPLIES (AND (MEMBER C (PLUS-FRINGE X))
			       (NUMBERP (MEANING C A)))
			  (NUMBERP (MEANING X A))))
    (PROVE-LEMMA CORRECTNESS-OF-CANCEL ((META EQUAL))
		 (IMPLIES (FORMP X)
			  (AND (EQUAL (MEANING X A)
				      (MEANING (CANCEL X)
					       A))
			       (FORMP (CANCEL X)))))
    (DEFN REVERSE (X)
      (IF (LISTP X)
	  (APPEND (REVERSE (CDR X))
		  (CONS (CAR X)
			NIL))
	  NIL))
    (PROVE-LEMMA ASSOCIATIVITY-OF-APPEND (REWRITE)
		 (EQUAL (APPEND (APPEND X Y)
				Z)
			(APPEND X (APPEND Y Z))))
    (DEFN PLISTP (X)
      (IF (LISTP X)
	  (PLISTP (CDR X))
	  (EQUAL X NIL)))
    (PROVE-LEMMA APPEND-RIGHT-ID (REWRITE)
		 (IMPLIES (PLISTP X)
			  (EQUAL (APPEND X NIL)
				 X)))
    (PROVE-LEMMA PLISTP-REVERSE (GENERALIZE REWRITE)
		 (PLISTP (REVERSE X)))
    (PROVE-LEMMA APPEND-REVERSE (REWRITE)
		 (EQUAL (REVERSE (APPEND A B))
			(APPEND (REVERSE B)
				(REVERSE A))))
    (PROVE-LEMMA TIMES-ZERO2 (REWRITE)
		 (IMPLIES (NOT (NUMBERP Y))
			  (EQUAL (TIMES X Y)
				 0)))
    (PROVE-LEMMA DISTRIBUTIVITY-OF-TIMES-OVER-PLUS (REWRITE)
		 (EQUAL (TIMES X (PLUS Y Z))
			(PLUS (TIMES X Y)
			      (TIMES X Z))))
    (PROVE-LEMMA TIMES-ADD1 (REWRITE)
		 (EQUAL (TIMES X (ADD1 Y))
			(IF (NUMBERP Y)
			    (PLUS X (TIMES X Y))
			    (FIX X))))
    (PROVE-LEMMA COMMUTATIVITY-OF-TIMES (REWRITE)
		 (EQUAL (TIMES X Y)
			(TIMES Y X)))
    (PROVE-LEMMA COMMUTATIVITY2-OF-TIMES (REWRITE)
		 (EQUAL (TIMES X (TIMES Y Z))
			(TIMES Y (TIMES X Z))))
    (PROVE-LEMMA ASSOCIATIVITY-OF-TIMES (REWRITE)
		 (EQUAL (TIMES (TIMES X Y)
			       Z)
			(TIMES X (TIMES Y Z))))
    (PROVE-LEMMA EQUAL-TIMES-0 (REWRITE)
		 (EQUAL (EQUAL (TIMES X Y)
			       0)
			(OR (ZEROP X)
			    (ZEROP Y))))
    (ADD-SHELL PUSH NIL STACKP ((TOP (NONE-OF)
				     ZERO)
				(POP (NONE-OF)
				     ZERO)))
    (DCL CALL (FN X Y))
    (DCL GETVALUE (VAR ENVRN))
    (ADD-AXIOM NUMBERP-CALL (REWRITE)
	       (NUMBERP (CALL FN X Y)))
    (DEFN
      EXPRESSIONP
      (X)
      (IF (LISTP X)
	  (IF (LISTP (CAR X))
	      F
	      (IF (LISTP (CDR X))
		  (IF (LISTP (CDDR X))
		      (IF (EXPRESSIONP (CADR X))
			  (EXPRESSIONP (CADDR X))
			  F)
		      F)
		  F))
	  T))
    (PROVE-LEMMA CADR-CROCK (REWRITE)
		 (IMPLIES (LISTP (CDDR X))
			  (LESSP (COUNT (CADR X))
				 (COUNT X))) 

;   This is trivial by CAR/CDR-ELIM.  However, in DEFN, when trying to prove
;   the lemmas that justify recursion, we use only SIMPLIFY. So we have to
;   prove this first.

		 )
    (DEFN EVAL (FORM ENVRN)
      (IF (NUMBERP FORM)
	  FORM
	  (IF (LISTP (CDDR FORM))
	      (CALL (CAR FORM)
		    (EVAL (CADR FORM)
			  ENVRN)
		    (EVAL (CADDR FORM)
			  ENVRN))
	      (GETVALUE FORM ENVRN))))
    (DEFN OPTIMIZE (FORM)
      (IF (LISTP (CDDR FORM))
	  (IF (NUMBERP (OPTIMIZE (CADR FORM)))
	      (IF (NUMBERP (OPTIMIZE (CADDR FORM)))
		  (CALL (CAR FORM)
			(OPTIMIZE (CADR FORM))
			(OPTIMIZE (CADDR FORM)))
		  (LIST (CAR FORM)
			(OPTIMIZE (CADR FORM))
			(OPTIMIZE (CADDR FORM))))
	      (LIST (CAR FORM)
		    (OPTIMIZE (CADR FORM))
		    (OPTIMIZE (CADDR FORM))))
	  FORM))
    (DEFN CODEGEN (FORM INS)
      (IF (NUMBERP FORM)
	  (CONS (LIST (QUOTE PUSHI)
		      FORM)
		INS)
	  (IF (LISTP (CDDR FORM))
	      (CONS (CAR FORM)
		    (CODEGEN (CADDR FORM)
			     (CODEGEN (CADR FORM)
				      INS)))
	      (CONS (LIST (QUOTE PUSHV)
			  FORM)
		    INS))))
    (DEFN COMPILE (FORM)
      (REVERSE (CODEGEN (OPTIMIZE FORM)
			NIL)))
    (PROVE-LEMMA FORMP-OPTIMIZE (REWRITE)
		 (IMPLIES (EXPRESSIONP X)
			  (EXPRESSIONP (OPTIMIZE X))))
    (PROVE-LEMMA CORRECTNESS-OF-OPTIMIZE (REWRITE)
		 (IMPLIES (EXPRESSIONP X)
			  (EQUAL (EVAL (OPTIMIZE X)
				       ENVRN)
				 (EVAL X ENVRN))))
    (DEFN
      EXEC
      (PC PDS ENVRN)
      (IF (NLISTP PC)
	  PDS
	  (IF (LISTP (CAR PC))
	      (IF (EQUAL (CAAR PC)
			 (QUOTE PUSHI))
		  (EXEC (CDR PC)
			(PUSH (CADAR PC)
			      PDS)
			ENVRN)
		  (EXEC (CDR PC)
			(PUSH (GETVALUE (CADAR PC)
					ENVRN)
			      PDS)
			ENVRN))
	      (EXEC (CDR PC)
		    (PUSH (CALL (CAR PC)
				(TOP (POP PDS))
				(TOP PDS))
			  (POP (POP PDS)))
		    ENVRN))))
    (PROVE-LEMMA SEQUENTIAL-EXECUTION (REWRITE)
		 (EQUAL (EXEC (APPEND X Y)
			      PDS ENVRN)
			(EXEC Y (EXEC X PDS ENVRN)
			      ENVRN)))
    (PROVE-LEMMA CORRECTNESS-OF-CODEGEN (REWRITE)
		 (IMPLIES (EXPRESSIONP X)
			  (EQUAL (EXEC (REVERSE (CODEGEN X INS))
				       PDS ENVRN)
				 (PUSH (EVAL X ENVRN)
				       (EXEC (REVERSE INS)
					     PDS ENVRN)))))
    (PROVE-LEMMA CORRECTNESS-OF-OPTIMIZING-COMPILER NIL
		 (IMPLIES (EXPRESSIONP X)
			  (EQUAL (EXEC (COMPILE X)
				       PDS ENVRN)
				 (PUSH (EVAL X ENVRN)
				       PDS))))
    (PROVE-LEMMA TRANSITIVITY-OF-LESSP NIL
		 (IMPLIES (AND (LESSP X Y)
			       (LESSP Y Z))
			  (LESSP X Z)))
    (PROVE-LEMMA LESSP-NOT-REFLEXIVE NIL (NOT (LESSP X X)))
    (DEFN EQP (X Y)
      (EQUAL (FIX X)
	     (FIX Y)))
    (PROVE-LEMMA TRICHOTOMY-OF-LESSP NIL
		 (IMPLIES (AND (NOT (EQP X Y))
			       (NOT (LESSP Y X)))
			  (LESSP X Y)))
    (PROVE-LEMMA REVERSE-REVERSE (REWRITE)
		 (IMPLIES (PLISTP X)
			  (EQUAL (REVERSE (REVERSE X))
				 X)))
    (DEFN FLATTEN (X)
      (IF (LISTP X)
	  (APPEND (FLATTEN (CAR X))
		  (FLATTEN (CDR X)))
	  (CONS X NIL)))
    (DEFN MC-FLATTEN (X Y)
      (IF (LISTP X)
	  (MC-FLATTEN (CAR X)
		      (MC-FLATTEN (CDR X)
				  Y))
	  (CONS X Y)))
    (PROVE-LEMMA FLATTEN-MC-FLATTEN (REWRITE)
		 (EQUAL (MC-FLATTEN X Y)
			(APPEND (FLATTEN X)
				Y)))
    (PROVE-LEMMA MEMBER-APPEND (REWRITE)
		 (EQUAL (MEMBER X (APPEND A B))
			(OR (MEMBER X A)
			    (MEMBER X B))))
    (PROVE-LEMMA MEMBER-REVERSE (REWRITE)
		 (EQUAL (MEMBER X (REVERSE Y))
			(MEMBER X Y)))
    (PROVE-LEMMA LENGTH-REVERSE (REWRITE)
		 (EQUAL (LENGTH (REVERSE X))
			(LENGTH X)))
    (DEFN INTERSECT (X Y)
      (IF (LISTP X)
	  (IF (MEMBER (CAR X)
		      Y)
	      (CONS (CAR X)
		    (INTERSECT (CDR X)
			       Y))
	      (INTERSECT (CDR X)
			 Y))
	  NIL))
    (PROVE-LEMMA MEMBER-INTERSECT (REWRITE)
		 (EQUAL (MEMBER A (INTERSECT B C))
			(AND (MEMBER A B)
			     (MEMBER A C))))
    (DEFN UNION (X Y)
      (IF (LISTP X)
	  (IF (MEMBER (CAR X)
		      Y)
	      (UNION (CDR X)
		     Y)
	      (CONS (CAR X)
		    (UNION (CDR X)
			   Y)))
	  Y))
    (PROVE-LEMMA MEMBER-UNION NIL (EQUAL (MEMBER A (UNION B C))
					 (OR (MEMBER A B)
					     (MEMBER A C))))
    (PROVE-LEMMA SUBSETP-UNION NIL (IMPLIES (SUBSETP A B)
					    (EQUAL (UNION A B)
						   B)))
    (PROVE-LEMMA SUBSETP-INTERSECT NIL
		 (IMPLIES (AND (PLISTP A)
			       (SUBSETP A B))
			  (EQUAL (INTERSECT A B)
				 A)))
    (DEFN NTH (X N)
      (IF (ZEROP N)
	  X
	  (NTH (CDR X)
	       (SUB1 N))))
    (DEFN GREATEREQP (X Y)
      (NOT (LESSP X Y)))
    (PROVE-LEMMA TRANSITIVITY-OF-LEQ NIL (IMPLIES (AND (LEQ X Y)
						       (LEQ Y Z))
						  (LEQ X Z)))
    (DEFN ORDERED (L)
      (IF (LISTP L)
	  (IF (LISTP (CDR L))
	      (IF (LESSP (CADR L)
			 (CAR L))
		  F
		  (ORDERED (CDR L)))
	      T)
	  T))
    (DEFN ADDTOLIST (X L)
      (IF (LISTP L)
	  (IF (LESSP X (CAR L))
	      (CONS X L)
	      (CONS (CAR L)
		    (ADDTOLIST X (CDR L))))
	  (CONS X NIL)))
    (DEFN SORT (L)
      (IF (LISTP L)
	  (ADDTOLIST (CAR L)
		     (SORT (CDR L)))
	  NIL))
    (DEFN ASSOC (X Y)
      (IF (LISTP Y)
	  (IF (EQUAL X (CAAR Y))
	      (CAR Y)
	      (ASSOC X (CDR Y)))
	  NIL))
    (DEFN BOOLEAN (X)
      (OR (EQUAL X T)
	  (EQUAL X F)))
    (DEFN IFF (X Y)
      (AND 
       (IMPLIES X Y)
       (IMPLIES Y X)))
    (PROVE-LEMMA IFF-EQUAL-EQUAL NIL (IMPLIES (AND (BOOLEAN P)
						   (BOOLEAN Q))
					      (EQUAL (IFF P Q)
						     (EQUAL P Q))))
    (PROVE-LEMMA NTH-0 (REWRITE)
		 (EQUAL (NTH 0 I)
			0))
    (PROVE-LEMMA NTH-NIL (REWRITE)
		 (EQUAL (NTH NIL I)
			(IF (ZEROP I)
			    NIL 0)))
    (PROVE-LEMMA NTH-APPEND1 (REWRITE)
		 (EQUAL (NTH A (PLUS I J))
			(NTH (NTH A I)
			     J)))
    (PROVE-LEMMA ASSOCIATIVITY-OF-EQUAL NIL
		 (IMPLIES (AND (BOOLEAN A)
			       (AND (BOOLEAN B)
				    (BOOLEAN C)))
			  (EQUAL (EQUAL (EQUAL A B)
					C)
				 (EQUAL A (EQUAL B C)))))
    (DEFN ODD (X)
      (IF (ZEROP X)
	  F
	  (IF (ZEROP (SUB1 X))
	      T
	      (ODD (SUB1 (SUB1 X))))))
    (DEFN EVEN1 (X)
      (IF (ZEROP X)
	  T
	  (ODD (SUB1 X))))
    (DEFN EVEN2 (X)
      (IF (ZEROP X)
	  T
	  (IF (ZEROP (SUB1 X))
	      F
	      (EVEN2 (SUB1 (SUB1 X))))))
    (DEFN DOUBLE (I)
      (IF (ZEROP I)
	  0
	  (ADD1 (ADD1 (DOUBLE (SUB1 I))))))
    (PROVE-LEMMA EVEN1-DOUBLE (REWRITE)
		 (EVEN1 (DOUBLE I)))
    (DEFN HALF (I)
      (IF (ZEROP I)
	  0
	  (IF (ZEROP (SUB1 I))
	      0
	      (ADD1 (HALF (SUB1 (SUB1 I)))))))
    (PROVE-LEMMA HALF-DOUBLE (REWRITE)
		 (IMPLIES (NUMBERP I)
			  (EQUAL (HALF (DOUBLE I))
				 I)))
    (PROVE-LEMMA DOUBLE-HALF (REWRITE)
		 (IMPLIES (AND (NUMBERP I)
			       (EVEN1 I))
			  (EQUAL (DOUBLE (HALF I))
				 I)))
    (PROVE-LEMMA DOUBLE-TIMES-2 NIL (EQUAL (DOUBLE I)
					   (TIMES 2 I)))
    (PROVE-LEMMA SUBSETP-CONS (REWRITE)
		 (IMPLIES (SUBSETP X Y)
			  (SUBSETP X (CONS Z Y))))
    (PROVE-LEMMA LAST-APPEND (REWRITE)
		 (EQUAL (LAST (APPEND A B))
			(IF (LISTP B)
			    (LAST B)
			    (IF (LISTP A)
				(CONS (CAR (LAST A))
				      B)
				B))))
    (PROVE-LEMMA LAST-REVERSE NIL
		 (IMPLIES (LISTP A)
			  (EQUAL (LAST (REVERSE A))
				 (CONS (CAR A)
				       NIL))))
    (DEFN EXP (I J)
      (IF (ZEROP J)
	  1
	  (TIMES I (EXP I (SUB1 J)))))
    (PROVE-LEMMA EXP-PLUS (REWRITE)
		 (EQUAL (EXP I (PLUS J K))
			(TIMES (EXP I J)
			       (EXP I K))))
    (PROVE-LEMMA EVEN1-EVEN2 NIL (EQUAL (EVEN1 X)
					(EVEN2 X)))
    (PROVE-LEMMA LEQ-NTH NIL (LEQ (LENGTH (NTH L I))
				  (LENGTH L)))
    (PROVE-LEMMA MEMBER-SORT NIL (EQUAL (MEMBER A (SORT B))
					(MEMBER A B)))
    (PROVE-LEMMA LENGTH-SORT NIL (EQUAL (LENGTH (SORT A))
					(LENGTH A)))
    (DEFN COUNT-LIST (A L)
      (IF (LISTP L)
	  (IF (EQUAL A (CAR L))
	      (ADD1 (COUNT-LIST A (CDR L)))
	      (COUNT-LIST A (CDR L)))
	  0))
    (PROVE-LEMMA COUNT-LIST-SORT NIL
		 (EQUAL (COUNT-LIST A (SORT L))
			(COUNT-LIST A L)))
    (PROVE-LEMMA ORDERED-APPEND NIL (IMPLIES
				      (ORDERED (APPEND A B))
				      (ORDERED A)))
    (PROVE-LEMMA LEQ-HALF NIL (LEQ (HALF I)
				   I))
    (DEFN NUMBER-LISTP (L)
      (IF (LISTP L)
	  (IF (NUMBERP (CAR L))
	      (NUMBER-LISTP (CDR L))
	      F)
	  (EQUAL L NIL)))
    (PROVE-LEMMA ORDERED-SORT (REWRITE)
		 (ORDERED (SORT X)))
    (PROVE-LEMMA ADDTOLIST-OF-ORDERED-NUMBER-LIST (REWRITE)
		 (IMPLIES (AND (ORDERED X)
			       (NUMBER-LISTP X)
			       (NUMBERP I)
			       (NOT (LESSP (CAR X)
					   I)))
			  (EQUAL (ADDTOLIST I X)
				 (CONS I X))))
    (PROVE-LEMMA SORT-OF-ORDERED-NUMBER-LIST (REWRITE)
		 (IMPLIES (AND (ORDERED X)
			       (NUMBER-LISTP X))
			  (EQUAL (SORT X)
				 X)))
    (DEFN XOR (P Q)
      (IF Q (IF P F T)
	  (EQUAL P T)))
    (PROVE-LEMMA CROCK-DUE-TO-LACK-OF-BOUNCE (REWRITE)
		 (IMPLIES (EQUAL X (SORT L))
			  (ORDERED X)))
    (PROVE-LEMMA SORT-ORDERED (REWRITE)
		 (IMPLIES (NUMBER-LISTP L)
			  (EQUAL (EQUAL (SORT L)
					L)
				 (ORDERED L))))
    (DEFN SUBST (X Y Z)
      (IF (EQUAL Y Z)
	  X
	  (IF (LISTP Z)
	      (CONS (SUBST X Y (CAR Z))
		    (SUBST X Y (CDR Z)))
	      Z)))
    (PROVE-LEMMA SUBST-A-A NIL (EQUAL (SUBST A A B)
				      B))
    (DEFN OCCUR (X Y)
      (IF (EQUAL X Y)
	  T
	  (IF (LISTP Y)
	      (IF (OCCUR X (CAR Y))
		  T
		  (OCCUR X (CDR Y)))
	      F)))
    (PROVE-LEMMA OCCUR-SUBST NIL (IMPLIES (NOT (OCCUR A B))
					  (EQUAL (SUBST C A B)
						 B)))
    (DEFN COUNTPS-LOOP (L PRED ANS)
      (IF (LISTP L)
	  (IF (CALL PRED (CAR L)
		    NIL)
	      (COUNTPS-LOOP (CDR L)
			    PRED
			    (ADD1 ANS))
	      (COUNTPS-LOOP (CDR L)
			    PRED ANS))
	  ANS))
    (DEFN COUNTPS- (L PRED)
      (COUNTPS-LOOP L PRED 0))
    (DEFN COUNTPS (L PRED)
      (IF (LISTP L)
	  (IF (CALL PRED (CAR L)
		    NIL)
	      (ADD1 (COUNTPS (CDR L)
			     PRED))
	      (COUNTPS (CDR L)
		       PRED))
	  0))
    (PROVE-LEMMA COUNTPS-COUNTPS (REWRITE)
		 (IMPLIES (NUMBERP N)
			  (EQUAL (COUNTPS-LOOP L PRED N)
				 (PLUS N (COUNTPS L PRED)))))
    (DEFN FACT (I)
      (IF (ZEROP I)
	  1
	  (TIMES I (FACT (SUB1 I)))))
    (DEFN FACT-LOOP (I ANS)
      (IF (ZEROP I)
	  ANS
	  (FACT-LOOP (SUB1 I)
		     (TIMES I ANS))))
    (DEFN FACT- (I)
      (FACT-LOOP I 1))
    (PROVE-LEMMA FACT-LOOP-FACT (REWRITE)
		 (IMPLIES (NUMBERP I)
			  (EQUAL (FACT-LOOP J I)
				 (TIMES I (FACT J)))))
    (PROVE-LEMMA FACT-FACT NIL (EQUAL (FACT- I)
				      (FACT I)))
    (DEFN REVERSE-LOOP (X ANS)
      (IF (LISTP X)
	  (REVERSE-LOOP (CDR X)
			(CONS (CAR X)
			      ANS))
	  ANS))
    (DEFN REVERSE- (X)
      (REVERSE-LOOP X NIL))
    (PROVE-LEMMA REVERSE-LOOP-APPEND-REVERSE (REWRITE)
		 (EQUAL (REVERSE-LOOP X Y)
			(APPEND (REVERSE X)
				Y)))
    (PROVE-LEMMA REVERSE-LOOP-REVERSE (REWRITE)
		 (EQUAL (REVERSE-LOOP X NIL)
			(REVERSE X)))
    (PROVE-LEMMA REVERSE-APPEND NIL (EQUAL (REVERSE- (APPEND A B))
					   (APPEND (REVERSE- B)
						   (REVERSE- A))))
    (PROVE-LEMMA REVERSE-REVERSE- NIL
		 (IMPLIES (PLISTP X)
			  (EQUAL (REVERSE- (REVERSE- X))
				 X)))
    (DEFN SORT-LP (X Y)
      (IF (LISTP X)
	  (SORT-LP (CDR X)
		   (ADDTOLIST (CAR X)
			      Y))
	  Y))
    (PROVE-LEMMA ORDERED-ADDTOLIST (REWRITE)
		 (IMPLIES (ORDERED Y)
			  (ORDERED (ADDTOLIST X Y))))
    (PROVE-LEMMA ORDERED-SORT-LP (REWRITE)
		 (IMPLIES (ORDERED Y)
			  (ORDERED (SORT-LP X Y))))
    (PROVE-LEMMA COUNT-SORT-LP (REWRITE)
		 (EQUAL (COUNT-LIST Z (SORT-LP X Y))
			(PLUS (COUNT-LIST Z X)
			      (COUNT-LIST Z Y))))
    (PROVE-LEMMA APPEND-CANCELLATION (REWRITE)
		 (EQUAL (EQUAL (APPEND A B)
			       (APPEND A C))
			(EQUAL B C)))
    (PROVE-LEMMA EQUAL-LESSP (REWRITE)
		 (EQUAL (EQUAL (LESSP X Y)
			       Z)
			(IF (LESSP X Y)
			    (EQUAL T Z)
			    (EQUAL F Z))))
    (PROVE-LEMMA DIFFERENCE-ELIM (ELIM)
		 (IMPLIES (AND (NUMBERP Y)
			       (NOT (LESSP Y X)))
			  (EQUAL (PLUS X (DIFFERENCE Y X))
				 Y)))
    (DEFN POWER-EVAL (L BASE)
      (IF (LISTP L)
	  (PLUS (CAR L)
		(TIMES BASE (POWER-EVAL (CDR L)
					BASE)))
	  0))
    (DEFN BIG-PLUS1 (L I BASE)
      (IF (LISTP L)
	  (IF (ZEROP I)
	      L
	      (CONS (REMAINDER (PLUS (CAR L)
				     I)
			       BASE)
		    (BIG-PLUS1 (CDR L)
			       (QUOTIENT (PLUS (CAR L)
					       I)
					 BASE)
			       BASE)))
	  (CONS I NIL)))
    (PROVE-LEMMA REMAINDER-QUOTIENT (REWRITE)
		 (EQUAL (PLUS (REMAINDER X Y)
			      (TIMES Y (QUOTIENT X Y)))
			(FIX X)))
    (PROVE-LEMMA POWER-EVAL-BIG-PLUS1 (REWRITE)
		 (EQUAL (POWER-EVAL (BIG-PLUS1 L I BASE)
				    BASE)
			(PLUS (POWER-EVAL L BASE)
			      I)))
    (DEFN
      BIG-PLUS
      (X Y I BASE)
      (IF (LISTP X)
	  (IF (LISTP Y)
	      (CONS (REMAINDER (PLUS I (PLUS (CAR X)
					     (CAR Y)))
			       BASE)
		    (BIG-PLUS (CDR X)
			      (CDR Y)
			      (QUOTIENT (PLUS I (PLUS (CAR X)
						      (CAR Y)))
					BASE)
			      BASE))
	      (BIG-PLUS1 X I BASE))
	  (BIG-PLUS1 Y I BASE)))
    (PROVE-LEMMA POWER-EVAL-BIG-PLUS (REWRITE)
		 (EQUAL (POWER-EVAL (BIG-PLUS X Y I BASE)
				    BASE)
			(PLUS I (PLUS (POWER-EVAL X BASE)
				      (POWER-EVAL Y BASE)))))
    (PROVE-LEMMA REMAINDER-WRT-1 (REWRITE)
		 (EQUAL (REMAINDER Y 1)
			0))
    (PROVE-LEMMA REMAINDER-WRT-12 (REWRITE)
		 (IMPLIES (NOT (NUMBERP X))
			  (EQUAL (REMAINDER Y X)
				 (FIX Y))))
    (PROVE-LEMMA LESSP-REMAINDER2 (REWRITE GENERALIZE)
		 (EQUAL (LESSP (REMAINDER X Y)
			       Y)
			(NOT (ZEROP Y))))
    (PROVE-LEMMA REMAINDER-X-X (REWRITE)
		 (EQUAL (REMAINDER X X)
			0))
    (PROVE-LEMMA REMAINDER-QUOTIENT-ELIM (ELIM)
		 (IMPLIES (AND (NOT (ZEROP Y))
			       (NUMBERP X))
			  (EQUAL (PLUS (REMAINDER X Y)
				       (TIMES Y (QUOTIENT X Y)))
				 X)))
    (PROVE-LEMMA LESSP-TIMES-1 (REWRITE)
		 (IMPLIES (NOT (ZEROP I))
			  (NOT (LESSP (TIMES I J)
				      J))))
    (PROVE-LEMMA LESSP-TIMES-2 (REWRITE)
		 (IMPLIES (NOT (ZEROP I))
			  (NOT (LESSP (TIMES J I)
				      J))))
    (PROVE-LEMMA LESSP-QUOTIENT1 (REWRITE)
		 (EQUAL (LESSP (QUOTIENT I J)
			       I)
			(AND (NOT (ZEROP I))
			     (OR (ZEROP J)
				 (NOT (EQUAL J 1))))))
    (PROVE-LEMMA LESSP-REMAINDER1 (REWRITE)
		 (EQUAL (LESSP (REMAINDER X Y)
			       X)
			(AND (NOT (ZEROP Y))
			     (NOT (ZEROP X))
			     (NOT (LESSP X Y)))))
    (DEFN POWER-REP (I BASE)
      (IF (ZEROP I)
	  NIL
	  (IF (ZEROP BASE)
	      (CONS I NIL)
	      (IF (EQUAL BASE 1)
		  (CONS I NIL)
		  (CONS (REMAINDER I BASE)
			(POWER-REP (QUOTIENT I BASE)
				   BASE))))))
    (PROVE-LEMMA POWER-EVAL-POWER-REP (REWRITE)
		 (EQUAL (POWER-EVAL (POWER-REP I BASE)
				    BASE)
			(FIX I)))
    (PROVE-LEMMA CORRECTNESS-OF-BIG-PLUS (REWRITE)
		 (EQUAL (POWER-EVAL (BIG-PLUS (POWER-REP I BASE)
					      (POWER-REP J BASE)
					      0 BASE)
				    BASE)
			(PLUS I J)))
    (DEFN GCD (X Y)
      (IF (ZEROP X)
	  (FIX Y)
	  (IF (ZEROP Y)
	      X
	      (IF (LESSP X Y)
		  (GCD X (DIFFERENCE Y X))
		  (GCD (DIFFERENCE X Y)
		       Y))))
      ((LEX2 (LIST (COUNT X)
		   (COUNT Y)))))
    (PROVE-LEMMA NUMBERP-GCD (REWRITE)
		 (NUMBERP (GCD X Y)))
    (PROVE-LEMMA GCD-EQUAL-0 (REWRITE)
		 (EQUAL (EQUAL (GCD X Y)
			       0)
			(AND (ZEROP X)
			     (ZEROP Y))))
    (PROVE-LEMMA GCD-0 (REWRITE)
		 (EQUAL (GCD 0 Y)
			(FIX Y)))
    (PROVE-LEMMA COMMUTATIVITY-OF-GCD (REWRITE)
		 (EQUAL (GCD X Y)
			(GCD Y X)))
    (PROVE-LEMMA NTH-APPEND (REWRITE)
		 (EQUAL (NTH (APPEND A B)
			     I)
			(APPEND (NTH A I)
				(NTH B (DIFFERENCE I (LENGTH A))))))
    (PROVE-LEMMA DIFFERENCE-PLUS1 (REWRITE)
		 (EQUAL (DIFFERENCE (PLUS X Y)
				    X)
			(FIX Y)))
    (PROVE-LEMMA DIFFERENCE-PLUS2 (REWRITE)
		 (EQUAL (DIFFERENCE (PLUS Y X)
				    X)
			(FIX Y)))
    (PROVE-LEMMA DIFFERENCE-PLUS-CANCELATION (REWRITE)
		 (EQUAL (DIFFERENCE (PLUS X Y)
				    (PLUS X Z))
			(DIFFERENCE Y Z)))
    (PROVE-LEMMA TIMES-DIFFERENCE (REWRITE)
		 (EQUAL (TIMES X (DIFFERENCE C W))
			(DIFFERENCE (TIMES C X)
				    (TIMES W X))))
    (DEFN DIVIDES (X Y)
      (ZEROP (REMAINDER Y X)))
    (PROVE-LEMMA DIVIDES-TIMES (REWRITE)
		 (EQUAL (REMAINDER (TIMES X Z)
				   Z)
			0))
    (PROVE-LEMMA DIFFERENCE-PLUS3 (REWRITE)
		 (EQUAL (DIFFERENCE (PLUS B (PLUS A C))
				    A)
			(PLUS B C)))
    (PROVE-LEMMA DIFFERENCE-ADD1-CANCELLATION (REWRITE)
		 (EQUAL (DIFFERENCE (ADD1 (PLUS Y Z))
				    Z)
			(ADD1 Y)))
    (PROVE-LEMMA REMAINDER-ADD1 (REWRITE)
		 (IMPLIES
		   (AND (NOT (ZEROP Y))
			(NOT (EQUAL Y 1)))
		   (NOT (EQUAL (REMAINDER (ADD1 (TIMES X Y))
					  Y)
			       0))))
    (PROVE-LEMMA DIVIDES-PLUS-REWRITE1 (REWRITE)
		 (IMPLIES (AND (EQUAL (REMAINDER X Z)
				      0)
			       (EQUAL (REMAINDER Y Z)
				      0))
			  (EQUAL (REMAINDER (PLUS X Y)
					    Z)
				 0)))
    (PROVE-LEMMA DIVIDES-PLUS-REWRITE2 (REWRITE)
		 (IMPLIES (AND (EQUAL (REMAINDER X Z)
				      0)
			       (NOT (EQUAL (REMAINDER Y Z)
					   0)))
			  (NOT (EQUAL (REMAINDER (PLUS X Y)
						 Z)
				      0))))
    (PROVE-LEMMA DIVIDES-PLUS-REWRITE (REWRITE)
		 (IMPLIES (EQUAL (REMAINDER X Z)
				 0)
			  (EQUAL (EQUAL (REMAINDER (PLUS X Y)
						   Z)
					0)
				 (EQUAL (REMAINDER Y Z)
					0))))
    (PROVE-LEMMA LESSP-PLUS-CANCELATION (REWRITE)
		 (EQUAL (LESSP (PLUS X Y)
			       (PLUS X Z))
			(LESSP Y Z)))
    (PROVE-LEMMA DIVIDES-PLUS-REWRITE-COMMUTED (REWRITE)
		 (IMPLIES (EQUAL (REMAINDER X Z)
				 0)
			  (EQUAL (EQUAL (REMAINDER (PLUS Y X)
						   Z)
					0)
				 (EQUAL (REMAINDER Y Z)
					0))))
    (PROVE-LEMMA EUCLID (REWRITE)
		 (IMPLIES
		   (EQUAL (REMAINDER X Z)
			  0)
		   (EQUAL (EQUAL (REMAINDER (DIFFERENCE Y X)
					    Z)
				 0)
			  (IF (LESSP X Y)
			      (EQUAL (REMAINDER Y Z)
				     0)
			      T))))
    (PROVE-LEMMA LESSP-TIMES-CANCELLATION (REWRITE)
		 (EQUAL (LESSP (TIMES X Z)
			       (TIMES Y Z))
			(AND (NOT (ZEROP Z))
			     (LESSP X Y))))
    (PROVE-LEMMA LESSP-PLUS-CANCELLATION3 (REWRITE)
		 (EQUAL (LESSP Y (PLUS X Y))
			(NOT (ZEROP X))))
    (PROVE-LEMMA DISTRIBUTIVITY-OF-TIMES-OVER-GCD (REWRITE)
		 (EQUAL (GCD (TIMES X Z)
			     (TIMES Y Z))
			(TIMES Z (GCD X Y))))
    (PROVE-LEMMA GCD-DIVIDES-BOTH (REWRITE)
		 (AND (EQUAL (REMAINDER X (GCD X Y))
			     0)
		      (EQUAL (REMAINDER Y (GCD X Y))
			     0)))
    (PROVE-LEMMA GCD-IS-THE-GREATEST NIL
		 (IMPLIES (AND (NOT (ZEROP X))
			       (NOT (ZEROP Y))
			       (DIVIDES Z X)
			       (DIVIDES Z Y))
			  (LEQ Z (GCD X Y))))
    (ADD-SHELL CONS-IF NIL IF-EXPRP ((TEST (NONE-OF)
					   ZERO)
				     (LEFT-BRANCH (NONE-OF)
						  ZERO)
				     (RIGHT-BRANCH (NONE-OF)
						   ZERO)))
    (DEFN ASSIGNMENT (VAR ALIST)
      (IF (EQUAL VAR T)
	  T
	  (IF (EQUAL VAR F)
	      F
	      (IF (NLISTP ALIST)
		  F
		  (IF (EQUAL VAR (CAAR ALIST))
		      (CDAR ALIST)
		      (ASSIGNMENT VAR (CDR ALIST)))))))
    (DEFN VALUE (X ALIST)
      (IF (IF-EXPRP X)
	  (IF (VALUE (TEST X)
		     ALIST)
	      (VALUE (LEFT-BRANCH X)
		     ALIST)
	      (VALUE (RIGHT-BRANCH X)
		     ALIST))
	  (ASSIGNMENT X ALIST)))
    (DEFN IF-DEPTH (X)
      (IF (IF-EXPRP X)
	  (ADD1 (IF-DEPTH (TEST X)))
	  0))
    (DEFN IF-COMPLEXITY (X)
      (IF (IF-EXPRP X)
	  (TIMES (IF-COMPLEXITY (TEST X))
		 (PLUS (IF-COMPLEXITY (LEFT-BRANCH X))
		       (IF-COMPLEXITY (RIGHT-BRANCH X))))
	  1))
    (PROVE-LEMMA IF-COMPLEXITY-NOT-0 (REWRITE)
		 (NOT (EQUAL (IF-COMPLEXITY X)
			     0)))
    (PROVE-LEMMA IF-COMPLEXITY-GOES-DOWN1 (REWRITE)
		 (IMPLIES (IF-EXPRP X)
			  (LESSP (IF-COMPLEXITY (LEFT-BRANCH X))
				 (IF-COMPLEXITY X))))
    (PROVE-LEMMA IF-COMPLEXITY-GOES-DOWN2 (REWRITE)
		 (IMPLIES (IF-EXPRP X)
			  (LESSP (IF-COMPLEXITY
				   (RIGHT-BRANCH X))
				 (IF-COMPLEXITY X))))
    (DEFN NORMALIZE
      (X)
      (IF (IF-EXPRP X)
	  (IF (IF-EXPRP (TEST X))
	      (NORMALIZE (CONS-IF (TEST (TEST X))
				  (CONS-IF
				    (LEFT-BRANCH (TEST X))
				    (LEFT-BRANCH X)
				    (RIGHT-BRANCH X))
				  (CONS-IF
				    (RIGHT-BRANCH (TEST X))
				    (LEFT-BRANCH X)
				    (RIGHT-BRANCH X))))
	      (CONS-IF (TEST X)
		       (NORMALIZE (LEFT-BRANCH X))
		       (NORMALIZE (RIGHT-BRANCH X))))
	  X)
      ((LEX2 (LIST (IF-COMPLEXITY X)
		   (IF-DEPTH X)))))
    (DEFN NORMALIZED-IF-EXPRP (X)
      (IF (IF-EXPRP X)
	  (AND (NOT (IF-EXPRP (TEST X)))
	       (NORMALIZED-IF-EXPRP (LEFT-BRANCH X))
	       (NORMALIZED-IF-EXPRP (RIGHT-BRANCH X)))
	  T))
    (DEFN ASSIGNEDP (VAR ALIST)
      (IF (EQUAL VAR T)
	  T
	  (IF (EQUAL VAR F)
	      T
	      (IF (NLISTP ALIST)
		  F
		  (IF (EQUAL VAR (CAAR ALIST))
		      T
		      (ASSIGNEDP VAR (CDR ALIST)))))))
    (DEFN ASSUME-TRUE (VAR ALIST)
      (CONS (CONS VAR T)
	    ALIST))
    (DEFN ASSUME-FALSE (VAR ALIST)
      (CONS (CONS VAR F)
	    ALIST))
    (DEFN TAUTOLOGYP (X ALIST)
      (IF (IF-EXPRP X)
	  (IF (ASSIGNEDP (TEST X)
			 ALIST)
	      (IF (ASSIGNMENT (TEST X)
			      ALIST)
		  (TAUTOLOGYP (LEFT-BRANCH X)
			      ALIST)
		  (TAUTOLOGYP (RIGHT-BRANCH X)
			      ALIST))
	      (AND (TAUTOLOGYP (LEFT-BRANCH X)
			       (ASSUME-TRUE (TEST X)
					    ALIST))
		   (TAUTOLOGYP (RIGHT-BRANCH X)
			       (ASSUME-FALSE (TEST X)
					     ALIST))))
	  (ASSIGNMENT X ALIST)))
    (PROVE-LEMMA ASSIGNMENT-APPEND (REWRITE)
		 (EQUAL (ASSIGNMENT X (APPEND A B))
			(IF (ASSIGNEDP X A)
			    (ASSIGNMENT X A)
			    (ASSIGNMENT X B))))
    (PROVE-LEMMA VALUE-CAN-IGNORE-REDUNDANT-ASSIGNMENTS (REWRITE)
		 (AND (IMPLIES (AND (IFF VAL (ASSIGNMENT VAR A))
				    (VALUE X A))
			       (VALUE X (CONS (CONS VAR VAL)
					      A)))
		      (IMPLIES (AND (IFF VAL (ASSIGNMENT VAR A))
				    (NOT (VALUE X A)))
			       (NOT (VALUE X (CONS (CONS VAR VAL)
						   A))))))
    (PROVE-LEMMA VALUE-SHORT-CUT (REWRITE)
		 (IMPLIES (AND (IF-EXPRP X)
			       (NORMALIZED-IF-EXPRP X))
			  (EQUAL (VALUE (TEST X)
					A)
				 (ASSIGNMENT (TEST X)
					     A))))
    (PROVE-LEMMA ASSIGNMENT-IMPLIES-ASSIGNED (REWRITE)
		 (IMPLIES (ASSIGNMENT X A)
			  (ASSIGNEDP X A)))
    (PROVE-LEMMA TAUTOLOGYP-IS-SOUND (REWRITE)
		 (IMPLIES (AND (NORMALIZED-IF-EXPRP X)
			       (TAUTOLOGYP X A1))
			  (VALUE X (APPEND A1 A2))))
    (DEFN TAUTOLOGY-CHECKER (X)
      (TAUTOLOGYP (NORMALIZE X)
		  NIL))
    (DEFN FALSIFY1 (X ALIST)
      (IF (IF-EXPRP X)
	  (IF (ASSIGNEDP (TEST X)
			 ALIST)
	      (IF (ASSIGNMENT (TEST X)
			      ALIST)
		  (FALSIFY1 (LEFT-BRANCH X)
			    ALIST)
		  (FALSIFY1 (RIGHT-BRANCH X)
			    ALIST))
	      (IF (FALSIFY1 (LEFT-BRANCH X)
			    (ASSUME-TRUE (TEST X)
					 ALIST))
		  (FALSIFY1 (LEFT-BRANCH X)
			    (ASSUME-TRUE (TEST X)
					 ALIST))
		  (FALSIFY1 (RIGHT-BRANCH X)
			    (ASSUME-FALSE (TEST X)
					  ALIST))))
	  (IF (ASSIGNEDP X ALIST)
	      (IF (ASSIGNMENT X ALIST)
		  F ALIST)
	      (CONS (CONS X F)
		    ALIST))))
    (DEFN FALSIFY (X)
      (FALSIFY1 (NORMALIZE X)
		NIL))
    (PROVE-LEMMA FALSIFY1-EXTENDS-MODELS (REWRITE)
		 (IMPLIES (ASSIGNEDP X A)
			  (EQUAL (ASSIGNMENT X (FALSIFY1 Y A))
				 (IF (FALSIFY1 Y A)
				     (ASSIGNMENT X A)
				     (EQUAL X T)))))
    (PROVE-LEMMA FALSIFY1-FALSIFIES (REWRITE)
		 (IMPLIES (AND (NORMALIZED-IF-EXPRP X)
			       (FALSIFY1 X A))
			  (EQUAL (VALUE X (FALSIFY1 X A))
				 F)))
    (PROVE-LEMMA TAUTOLOGYP-FAILS-MEANS-FALSIFY1-WINS (REWRITE)
		 (IMPLIES (AND (NORMALIZED-IF-EXPRP X)
			       (NOT (TAUTOLOGYP X A))
			       A)
			  (FALSIFY1 X A)))
    (PROVE-LEMMA NORMALIZE-IS-SOUND (REWRITE)
		 (EQUAL (VALUE (NORMALIZE X)
			       A)
			(VALUE X A)))
    (PROVE-LEMMA NORMALIZE-NORMALIZES (REWRITE)
		 (NORMALIZED-IF-EXPRP (NORMALIZE X)))
    (PROVE-LEMMA TAUTOLOGY-CHECKER-COMPLETENESS-BRIDGE (REWRITE)
		 (IMPLIES (AND (EQUAL (VALUE Y (FALSIFY1 X A))
				      (VALUE X (FALSIFY1 X A)))
			       (FALSIFY1 X A)
			       (NORMALIZED-IF-EXPRP X))
			  (EQUAL (VALUE Y (FALSIFY1 X A))
				 F)))
    (PROVE-LEMMA TAUTOLOGY-CHECKER-IS-COMPLETE NIL
		 (IMPLIES (NOT (TAUTOLOGY-CHECKER X))
			  (EQUAL (VALUE X (FALSIFY X))
				 F)))
    (PROVE-LEMMA TAUTOLOGY-CHECKER-SOUNDNESS-BRIDGE (REWRITE)
		 (IMPLIES (AND (TAUTOLOGYP Y A1)
			       (NORMALIZED-IF-EXPRP Y)
			       (EQUAL (VALUE X A2)
				      (VALUE Y (APPEND A1 A2))))
			  (VALUE X A2)))
    (PROVE-LEMMA TAUTOLOGY-CHECKER-IS-SOUND NIL
		 (IMPLIES (TAUTOLOGY-CHECKER X)
			  (VALUE X A)))
;;     (SWAP-OUT "P-TEMP")
       (MAKE-LIB "P-TEMP") 
       (NOTE-LIB "P-TEMP.LIB" "P-TEMP.LISP")
    (PROVE-LEMMA FLATTEN-SINGLETON (REWRITE)
		 (EQUAL (EQUAL (FLATTEN X)
			       (CONS Y NIL))
			(AND (NLISTP X)
			     (EQUAL X Y))))
    (DEFN LEFTCOUNT (X)
      (IF (NLISTP X)
	  0
	  (ADD1 (LEFTCOUNT (CAR X)))))
    (DEFN GOPHER (X)
      (IF (OR (NLISTP X)
	      (NLISTP (CAR X)))
	  X
	  (GOPHER (CONS (CAAR X)
			(CONS (CDAR X)
			      (CDR X)))))
      ((LESSP (LEFTCOUNT X))))
    (PROVE-LEMMA GOPHER-PRESERVES-COUNT (REWRITE)
		 (NOT (LESSP (COUNT X)
			     (COUNT (GOPHER X)))))
    (PROVE-LEMMA LISTP-GOPHER (REWRITE)
		 (EQUAL (LISTP (GOPHER X))
			(LISTP X)))
    (DEFN SAMEFRINGE (X Y)
      (IF (OR (NLISTP X)
	      (NLISTP Y))
	  (EQUAL X Y)
	  (AND (EQUAL (CAR (GOPHER X))
		      (CAR (GOPHER Y)))
	       (SAMEFRINGE (CDR (GOPHER X))
			   (CDR (GOPHER Y))))))
    (PROVE-LEMMA GOPHER-RETURNS-LEFTMOST-ATOM (REWRITE)
		 (EQUAL (CAR (GOPHER X))
			(IF (LISTP X)
			    (CAR (FLATTEN X))
			    0)))
    (PROVE-LEMMA GOPHER-RETURNS-CORRECT-STATE (REWRITE)
		 (EQUAL (FLATTEN (CDR (GOPHER X)))
			(IF (LISTP X)
			    (CDR (FLATTEN X))
			    (CONS 0 NIL))))
    (PROVE-LEMMA CORRECTNESS-OF-SAMEFRINGE (REWRITE)
		 (EQUAL (SAMEFRINGE X Y)
			(EQUAL (FLATTEN X)
			       (FLATTEN Y))))
    (DEFN PRIME1 (X Y)
      (IF (ZEROP Y)
	  F
	  (IF (EQUAL Y 1)
	      T
	      (AND (NOT (DIVIDES Y X))
		   (PRIME1 X (SUB1 Y))))))
    (DEFN PRIME (X)
      (AND (NOT (ZEROP X))
	   (NOT (EQUAL X 1))
	   (PRIME1 X (SUB1 X))))
    (DEFN GREATEST-FACTOR (X Y)
      (IF (OR (ZEROP Y)
	      (EQUAL Y 1))
	  X
	  (IF (DIVIDES Y X)
	      Y
	      (GREATEST-FACTOR X (SUB1 Y)))))
    (PROVE-LEMMA GREATEST-FACTOR-LESSP (REWRITE)
		 (IMPLIES (AND (LESSP Y X)
			       (NOT (PRIME1 X Y))
			       (NOT (ZEROP X))
			       (NOT (EQUAL (SUB1 X)
					   0))
			       (NOT (ZEROP Y)))
			  (LESSP (GREATEST-FACTOR X Y)
				 X)))
    (PROVE-LEMMA GREATEST-FACTOR-DIVIDES (REWRITE)
		 (IMPLIES (AND (LESSP Y X)
			       (NOT (PRIME1 X Y))
			       (NOT (ZEROP X))
			       (NOT (EQUAL X 1))
			       (NOT (ZEROP Y)))
			  (EQUAL (REMAINDER X
					    (GREATEST-FACTOR X Y))
				 0)))
    (PROVE-LEMMA GREATEST-FACTOR-0 (REWRITE)
		 (EQUAL (EQUAL (GREATEST-FACTOR X Y)
			       0)
			(AND (OR (ZEROP Y)
				 (EQUAL Y 1))
			     (EQUAL X 0))))
    (PROVE-LEMMA REMAINDER-0-CROCK (REWRITE)
		 (EQUAL (REMAINDER 0 Y)
			0)
		 NIL

;   We have to prove this to get (REMAINDER 1 Y) to open in GREATEST-FACTOR-1.
;   If CURRENT-CL moved we wouldn't have to do it.

		 )
    (PROVE-LEMMA GREATEST-FACTOR-1 (REWRITE)
		 (EQUAL (EQUAL (GREATEST-FACTOR X Y)
			       1)
			(EQUAL X 1)))
    (PROVE-LEMMA NUMBERP-GREATEST-FACTOR (REWRITE)
		 (EQUAL (NUMBERP (GREATEST-FACTOR X Y))
			(NOT (AND (OR (ZEROP Y)
				      (EQUAL Y 1))
				  (NOT (NUMBERP X))))))
    (DEFN
      PRIME-FACTORS
      (X)
      (IF (OR (ZEROP X)
	      (EQUAL (SUB1 X)
		     0))
	  NIL
	  (IF (PRIME1 X (SUB1 X))
	      (CONS X NIL)
	      (APPEND (PRIME-FACTORS (GREATEST-FACTOR X
						      (SUB1 X)))
		      (PRIME-FACTORS
			(QUOTIENT X (GREATEST-FACTOR X (SUB1 X))))))))
    (DEFN PRIME-LIST (L)
      (IF (NLISTP L)
	  T
	  (AND (PRIME (CAR L))
	       (PRIME-LIST (CDR L)))))
    (DEFN TIMES-LIST (L)
      (IF (NLISTP L)
	  1
	  (TIMES (CAR L)
		 (TIMES-LIST (CDR L)))))
    (PROVE-LEMMA TIMES-LIST-APPEND (REWRITE)
		 (EQUAL (TIMES-LIST (APPEND X Y))
			(TIMES (TIMES-LIST X)
			       (TIMES-LIST Y))))
    (PROVE-LEMMA PRIME-LIST-APPEND (REWRITE)
		 (EQUAL (PRIME-LIST (APPEND X Y))
			(AND (PRIME-LIST X)
			     (PRIME-LIST Y))))
    (PROVE-LEMMA PRIME-LIST-PRIME-FACTORS (REWRITE)
		 (PRIME-LIST (PRIME-FACTORS X)))
    (PROVE-LEMMA QUOTIENT-TIMES1 (REWRITE)
		 (IMPLIES (AND (NUMBERP Y)
			       (NUMBERP X)
			       (NOT (EQUAL X 0))
			       (DIVIDES X Y))
			  (EQUAL (TIMES X (QUOTIENT Y X))
				 Y)))
    (PROVE-LEMMA QUOTIENT-LESSP (REWRITE)
		 (IMPLIES (AND (NOT (ZEROP X))
			       (LESSP X Y))
			  (NOT (EQUAL (QUOTIENT Y X)
				      0))))
    (PROVE-LEMMA ENOUGH-FACTORS (REWRITE)
		 (IMPLIES (NOT (ZEROP X))
			  (EQUAL (TIMES-LIST (PRIME-FACTORS X))
				 X)))
    (PROVE-LEMMA PRIME-FACTORIZATION-EXISTENCE NIL
		 (IMPLIES
		   (NOT (ZEROP X))
		   (AND (EQUAL (TIMES-LIST (PRIME-FACTORS X))
			       X)
			(PRIME-LIST (PRIME-FACTORS X)))))
    (DEFN GREATEREQPR (W Z)
      (IF (ZEROP W)
	  (ZEROP Z)
	  (IF (EQUAL W Z)
	      T
	      (GREATEREQPR (SUB1 W)
			   Z))))
    (PROVE-LEMMA TIMES-ID-IFF-1 (REWRITE)
		 (EQUAL (EQUAL Z (TIMES W Z))
			(AND (NUMBERP Z)
			     (OR (EQUAL Z 0)
				 (EQUAL W 1)))))
    (PROVE-LEMMA PRIME1-BASIC (REWRITE)
		 (IMPLIES (AND (NOT (EQUAL Z 1))
			       (NOT (EQUAL Z 0))
			       (NUMBERP Z)
			       (GREATEREQPR U Z))
			  (NOT (PRIME1 (TIMES W Z)
				       U))))
    (PROVE-LEMMA GREATEREQPR-LESSP (REWRITE)
		 (EQUAL (GREATEREQPR X Y)
			(NOT (LESSP X Y))))
    (PROVE-LEMMA GREATEREQPR-REMAINDER (REWRITE)
		 (IMPLIES (AND (NOT (EQUAL Z (ADD1 V)))
			       (DIVIDES Z (ADD1 V)))
			  (GREATEREQPR V Z)))
    (PROVE-LEMMA PRIME-BASIC (REWRITE)
		 (IMPLIES (AND (NOT (EQUAL Z 1))
			       (NOT (EQUAL Z X))
			       (NOT (ZEROP X))
			       (NOT (EQUAL X 1))
			       (DIVIDES Z X))
			  (NOT (PRIME1 X (SUB1 X)))))
    (PROVE-LEMMA REMAINDER-GCD (REWRITE)
		 (IMPLIES (EQUAL (GCD B X)
				 Y)
			  (EQUAL (REMAINDER B Y)
				 0)))
    (PROVE-LEMMA REMAINDER-GCD-1 (REWRITE)
		 (IMPLIES (NOT (EQUAL (REMAINDER B X)
				      0))
			  (NOT (EQUAL (GCD B X)
				      X))))
    (PROVE-LEMMA DIVIDES-TIMES1 (REWRITE)
		 (IMPLIES (EQUAL A (TIMES Z Y))
			  (EQUAL (REMAINDER A Z)
				 0)))
    (PROVE-LEMMA TIMES-IDENTITY1 (REWRITE)
		 (IMPLIES (AND (NUMBERP Y)
			       (NOT (EQUAL Y 1))
			       (NOT (EQUAL Y 0))
			       (NOT (EQUAL X 0)))
			  (NOT (EQUAL X (TIMES X Y)))))
    (PROVE-LEMMA TIMES-IDENTITY (REWRITE)
		 (EQUAL (EQUAL X (TIMES X Y))
			(OR (EQUAL X 0)
			    (AND (NUMBERP X)
				 (EQUAL Y 1)))))
    (PROVE-LEMMA KLUDGE-BRIDGE (REWRITE)
		 (IMPLIES (EQUAL Y (TIMES K X))
			  (EQUAL (GCD Y (TIMES A X))
				 (TIMES X (GCD A K)))))
    (PROVE-LEMMA HACK1 (REWRITE)
		 (IMPLIES (AND (NOT (DIVIDES X A))
			       (EQUAL A (GCD (TIMES X A)
					     (TIMES B A))))
			  (NOT (EQUAL (TIMES K X)
				      (TIMES B A)))))
    (PROVE-LEMMA PRIME-GCD (REWRITE)
		 (IMPLIES (AND (NOT (DIVIDES X B))
			       (NOT (ZEROP X))
			       (NOT (EQUAL (SUB1 X)
					   0))
			       (PRIME1 X (SUB1 X)))
			  (EQUAL (EQUAL (GCD B X)
					1)
				 T))
		 NIL

;   The third hyp is that X is not 1; we have phrased it oddly on purpose. The
;   more natural phrasing causes us to fail to prove this theorem. The problem
;   is that the proof requires an appeal to PRIME-BASIC in which the free var Z
;   is instantiated to be (GCD B X) -- which is guessed by instantiating the
;   hyp (NOT (EQUAL Z 1)) and that instantiation is screwed if we put among our
;   hyps (NOT (EQUAL X 1)).

		 )
    (PROVE-LEMMA GCD-DISTRIBUTES-OVER-AN-OPENED-UP-TIMES (REWRITE)
		 (IMPLIES (AND (NUMBERP X)
			       (NOT (EQUAL X 0))
			       (EQUAL FREE (TIMES X Z)))
			  (EQUAL (GCD (TIMES B Z)
				      FREE)
				 (TIMES Z (GCD B X))))
		 NIL

;   As is evident from the name, this stupid lemma is necessary because of a
;   Knuth-Bendix type problem. Had X*Z not been expanded we could have used the
;   more elegant DISTRIBUTIVITY-OF-TIMES-OVER-GCD. This lemma has a further
;   twist. X is a free var. to cut down on the frequency with which this lemma
;   is tried. Once, (NOT (EQUAL X 0)) was the first hyp. It happened that in
;   there were three possibly choices for X from the TYPE-ALIST at run time,
;   but that the first one was correct. Unfortunately, when we changed the
;   order of evaluation of the lits in a clause, the correct choice was
;   obscured. Luckily, by keying on the NUMBERP hyp we can still get the tp to
;   chose the right X. The other two choices are both numeric -- they are
;   REMAINDER expressions -- but the fact that they are numeric is not stored
;   on the TYPE-ALIST, thank goodness! Isn't that dreadful?

		 )
    (PROVE-LEMMA PRIME-KEY (REWRITE)
		 (IMPLIES (AND (NUMBERP Z)
			       (PRIME X)
			       (NOT (DIVIDES X Z))
			       (NOT (DIVIDES X B)))
			  (NOT (EQUAL (TIMES X K)
				      (TIMES B Z)))))
    (PROVE-LEMMA
      QUOTIENT-DIVIDES
      (REWRITE)
      (IMPLIES (AND (NUMBERP Y)
		    (NOT (EQUAL (TIMES X (QUOTIENT Y X))
				Y)))
	       (NOT (EQUAL (REMAINDER Y X)
			   0))))
    (PROVE-LEMMA LITTLE-STEP (REWRITE)
		 (IMPLIES (AND (PRIME X)
			       (NOT (EQUAL Y 1))
			       (NOT (EQUAL X Y)))
			  (NOT (EQUAL (REMAINDER X Y)
				      0))))
    (PROVE-LEMMA LESSP-COUNT-DELETE (REWRITE)
		 (IMPLIES (MEMBER N L)
			  (LESSP (COUNT (DELETE N L))
				 (COUNT L))))
    (DEFN PERM (A B)
      (IF (NLISTP A)
	  (NLISTP B)
	  (IF (MEMBER (CAR A)
		      B)
	      (PERM (CDR A)
		    (DELETE (CAR A)
			    B))
	      F)))
    (PROVE-LEMMA REMAINDER-TIMES (REWRITE)
		 (EQUAL (REMAINDER (TIMES Y X)
				   Y)
			0))
    (PROVE-LEMMA PRIME-LIST-DELETE (REWRITE)
		 (IMPLIES (PRIME-LIST L2)
			  (PRIME-LIST (DELETE X L2))))
    (PROVE-LEMMA DIVIDES-TIMES-LIST (REWRITE)
		 (IMPLIES (AND (NOT (ZEROP C))
			       (MEMBER C L))
			  (EQUAL (REMAINDER (TIMES-LIST L)
					    C)
				 0)))
    (PROVE-LEMMA QUOTIENT-TIMES (REWRITE)
		 (EQUAL (QUOTIENT (TIMES Y X)
				  Y)
			(IF (ZEROP Y)
			    0
			    (FIX X))))
    (PROVE-LEMMA DISTRIBUTIVITY-OF-DIVIDES (REWRITE)
		 (IMPLIES (AND (NOT (ZEROP A))
			       (DIVIDES A W))
			  (EQUAL (TIMES C (QUOTIENT W A))
				 (QUOTIENT (TIMES C W)
					   A))))
    (PROVE-LEMMA TIMES-LIST-DELETE (REWRITE)
		 (IMPLIES (AND (NOT (ZEROP C))
			       (MEMBER C L))
			  (EQUAL (TIMES-LIST (DELETE C L))
				 (QUOTIENT (TIMES-LIST L)
					   C))))
    (PROVE-LEMMA PRIME-LIST-TIMES-LIST (REWRITE)
		 (IMPLIES
		   (AND (PRIME C)
			(PRIME-LIST L2)
			(NOT (MEMBER C L2)))
		   (NOT (EQUAL (REMAINDER (TIMES-LIST L2)
					  C)
			       0))))
    (PROVE-LEMMA IF-TIMES-THEN-DIVIDES (REWRITE)
		 (IMPLIES (AND (NOT (ZEROP C))
			       (NOT (DIVIDES C X)))
			  (NOT (EQUAL (TIMES C Y)
				      X))))
    (PROVE-LEMMA TIMES-EQUAL-1 (REWRITE)
		 (EQUAL (EQUAL (TIMES A B)
			       1)
			(AND (NOT (EQUAL A 0))
			     (NOT (EQUAL B 0))
			     (NUMBERP A)
			     (NUMBERP B)
			     (EQUAL (SUB1 A)
				    0)
			     (EQUAL (SUB1 B)
				    0))))
    (PROVE-LEMMA PRIME-MEMBER (REWRITE)
			   (IMPLIES (AND (EQUAL (TIMES C (TIMES-LIST L1))
						(TIMES-LIST L2))
					 (PRIME C)
					 (PRIME-LIST L2))
				    (MEMBER C L2))
			   ((DISABLE TIMES)))
    (PROVE-LEMMA DIVIDES-IMPLIES-TIMES (REWRITE)
		 (IMPLIES (AND (NOT (ZEROP A))
			       (NUMBERP C)
			       (EQUAL (TIMES A C)
				      B))
			  (EQUAL (EQUAL C (QUOTIENT B A))
				 T)))
    (PROVE-LEMMA PRIME-FACTORIZATION-UNIQUENESS NIL
		 (IMPLIES (AND (PRIME-LIST L1)
			       (PRIME-LIST L2)
			       (EQUAL (TIMES-LIST L1)
				      (TIMES-LIST L2)))
			  (PERM L1 L2)))
    (DEFN MAXIMUM (L)
      (IF (NLISTP L)
	  0
	  (IF (LESSP (CAR L)
		     (MAXIMUM (CDR L)))
	      (MAXIMUM (CDR L))
	      (CAR L))))
    (PROVE-LEMMA MEMBER-MAXIMUM (REWRITE)
		 (IMPLIES (LISTP X)
			  (MEMBER (MAXIMUM X)
				  X)))
    (PROVE-LEMMA LESSP-DELETE-REWRITE (REWRITE)
		 (EQUAL (LESSP (COUNT (DELETE X L))
			       (COUNT L))
			(MEMBER X L)))
    (DEFN ORDERED2 (L)
      (IF (LISTP L)
	  (IF (LISTP (CDR L))
	      (IF (LESSP (CAR L)
			 (CADR L))
		  F
		  (ORDERED2 (CDR L)))
	      T)
	  T))
    (DEFN DSORT (L)
      (IF (NLISTP L)
	  NIL
	  (CONS (MAXIMUM L)
		(DSORT (DELETE (MAXIMUM L)
			       L)))))
    (DEFN ADDTOLIST2 (X L)
      (IF (LISTP L)
	  (IF (LESSP X (CAR L))
	      (CONS (CAR L)
		    (ADDTOLIST2 X (CDR L)))
	      (CONS X L))
	  (CONS X NIL)))
    (DEFN SORT2 (L)
      (IF (NLISTP L)
	  NIL
	  (ADDTOLIST2 (CAR L)
		      (SORT2 (CDR L)))))
    (PROVE-LEMMA SORT2-GEN-1 (REWRITE)
		 (PLISTP (SORT2 X)))
    (PROVE-LEMMA SORT2-GEN-2 (REWRITE)
		 (ORDERED2 (SORT2 X)))
    (PROVE-LEMMA SORT2-GEN (GENERALIZE)
		 (AND (PLISTP (SORT2 X))
		      (ORDERED2 (SORT2 X))))
    (PROVE-LEMMA ADDTOLIST2-DELETE (REWRITE)
		 (IMPLIES (AND (PLISTP Y)
			       (ORDERED2 Y)
			       (NOT (EQUAL X V)))
			  (EQUAL (ADDTOLIST2 V (DELETE X Y))
				 (DELETE X (ADDTOLIST2 V Y)))))
    (PROVE-LEMMA DELETE-ADDTOLIST2 (REWRITE)
		 (IMPLIES (PLISTP Y)
			  (EQUAL (DELETE V (ADDTOLIST2 V Y))
				 Y)))
    (PROVE-LEMMA ADDTOLIST2-KLUDGE (REWRITE)
		 (IMPLIES (AND (NOT (LESSP V W))
			       (EQUAL (ADDTOLIST2 V Y)
				      (CONS V Y)))
			  (EQUAL (ADDTOLIST2 V (ADDTOLIST2 W Y))
				 (CONS V (ADDTOLIST2 W Y)))))
    (PROVE-LEMMA LESSP-MAXIMUM-ADDTOLIST2 (REWRITE)
		 (IMPLIES (NOT (LESSP V (MAXIMUM Z)))
			  (EQUAL (ADDTOLIST2 V (SORT2 Z))
				 (CONS V (SORT2 Z)))))
    (PROVE-LEMMA SORT2-DELETE-CONS (REWRITE)
		 (IMPLIES (LISTP X)
			  (EQUAL (CONS (MAXIMUM X)
				       (DELETE (MAXIMUM X)
					       (SORT2 X)))
				 (SORT2 X))))
    (PROVE-LEMMA SORT2-DELETE (REWRITE)
		 (EQUAL (SORT2 (DELETE X L))
			(DELETE X (SORT2 L))))
    (PROVE-LEMMA DSORT-SORT2 (REWRITE)
		 (EQUAL (DSORT X)
			(SORT2 X)))
    (PROVE-LEMMA COUNT-LIST-SORT2 NIL
		 (EQUAL (COUNT-LIST A (SORT2 L))
			(COUNT-LIST A L)))

;   The next segment of this XXX illustrates three different program
;   verification methods:  the functional approach, the inductive assertion
;   approach, and the interpreter approach.  The program considered is a simple
;   loop for summing the numbers from I down to 0
    
    (DEFN SIGMA (M N)
      (IF (LESSP M N)
	  (PLUS N (SIGMA M (SUB1 N)))
	  0)
      NIL

;   With each program verification method we will prove that the program
;   computes (SIGMA 0 I); at the end of this exercise we prove that (SIGMA 0 I)
;   is I*I+1/2.

      )
    (PROVE-LEMMA DIFFERENCE-1 (REWRITE)
		 (EQUAL (DIFFERENCE X 1)
			(SUB1 X)))
    (DEFN PROG-TRANS-OF-SIGMA (I AC)
      (IF (ZEROP I)
	  AC
	  (PROG-TRANS-OF-SIGMA (DIFFERENCE I 1)
			       (PLUS AC I))))
    (PROVE-LEMMA FUNCTIONAL-LOOP-INVRT (REWRITE)
		 (IMPLIES (NUMBERP AC)
			  (EQUAL (PROG-TRANS-OF-SIGMA I AC)
				 (PLUS AC (SIGMA 0 I)))))
    (PROVE-LEMMA CORRECTNESS-OF-FUNCTIONAL-SIGMA NIL
		 (EQUAL (PROG-TRANS-OF-SIGMA I 0)
			(SIGMA 0 I)))
    (PROVE-LEMMA SIGMA-INPUT-PATH NIL (AND (EQUAL 0 (SIGMA K K))
					   (LEQ K K)))
    (PROVE-LEMMA SIGMA-LOOP-INVRT NIL
		 (IMPLIES (AND (NOT (ZEROP I))
			       (LEQ I K))
			  (AND (EQUAL (PLUS (SIGMA I K)
					    I)
				      (SIGMA (SUB1 I)
					     K))
			       (LEQ (SUB1 I)
				    K))))
    (PROVE-LEMMA SIGMA-OUTPUT-PATH NIL
		 (IMPLIES (AND (ZEROP I)
			       (LEQ I K))
			  (EQUAL (SIGMA I K)
				 (SIGMA 0 K))))

;   The interpreter we consider fetches instructions out of the same memory
;   being modified by the execution.  Earlier we proved a simpler version in
;   which the program was in read-only memory.  The new approach is almost
;   identical but we have to force the opening up of certain functions because
;   instead of doing CDR recursion the interpreter EXECUTE1 has to count the PC
;   up and the theorem prover doesn't handle counting up very well yet.
    
    (DEFN SET (ADDR VAL MEM)
      (IF (ZEROP ADDR)
	  (CONS VAL (CDR MEM))
	  (CONS (CAR MEM)
		(SET (SUB1 ADDR)
		     VAL
		     (CDR MEM)))))
    (DEFN GET (ADDR MEM)
      (IF (ZEROP ADDR)
	  (CAR MEM)
	  (GET (SUB1 ADDR)
	       (CDR MEM))))
    (PROVE-LEMMA GET-SET (REWRITE)
		 (EQUAL (GET J (SET I VAL MEM))
			(IF (EQP J I)
			    VAL
			    (GET J MEM))))
    (DEFN
      EXECUTE1
      (PC MEM MAX)
      (IF
	(NOT (LESSP PC MAX))
	(LIST F MEM)
	(IF
	  (EQUAL (GET PC MEM)
		 (QUOTE (STOP)))
	  (LIST F MEM)
	  (IF
	    (EQUAL (CAR (GET PC MEM))
		   (QUOTE JUMPA))
	    (LIST (CADR (GET PC MEM))
		  MEM)
	    (IF
	      (EQUAL (CAR (GET PC MEM))
		     (QUOTE SKIPNE))
	      (IF (ZEROP (GET (CADR (GET PC MEM))
			      MEM))
		  (EXECUTE1 (ADD1 PC)
			    MEM MAX)
		  (EXECUTE1 (ADD1 (ADD1 PC))
			    MEM MAX))
	      (IF
		(EQUAL (CAR (GET PC MEM))
		       (QUOTE SUBI))
		(EXECUTE1 (ADD1 PC)
			  (SET (CADR (GET PC MEM))
			       (DIFFERENCE (GET (CADR (GET PC MEM))
						MEM)
					   (CADDR (GET PC MEM)))
			       MEM)
			  MAX)
		(IF
		  (EQUAL (CAR (GET PC MEM))
			 (QUOTE ADDI))
		  (EXECUTE1 (ADD1 PC)
			    (SET (CADR (GET PC MEM))
				 (PLUS (CADDR (GET PC MEM))
				       (GET (CADR (GET PC MEM))
					    MEM))
				 MEM)
			    MAX)
		  (IF (EQUAL (CAR (GET PC MEM))
			     (QUOTE ADD))
		      (EXECUTE1
			(ADD1 PC)
			(SET (CADR (GET PC MEM))
			     (PLUS (GET (CADDR (GET PC MEM))
					MEM)
				   (GET (CADR (GET PC MEM))
					MEM))
			     MEM)
			MAX)
		      (IF (EQUAL (CAR (GET PC MEM))
				 (QUOTE MOVEI))
			  (EXECUTE1 (ADD1 PC)
				    (SET (CADR (GET PC MEM))
					 (CADDR (GET PC MEM))
					 MEM)
				    MAX)
			  (LIST F MEM)))))))))
      ((LESSP (DIFFERENCE MAX PC))))
    (DEFN EXECUTE (PC MEM CLK)
      (IF (ZEROP CLK)
	  MEM
	  (IF (NUMBERP PC)
	      (EXECUTE (CAR (EXECUTE1 PC MEM (LENGTH MEM)))
		       (CADR (EXECUTE1 PC MEM (LENGTH MEM)))
		       (SUB1 CLK))
	      MEM)))
    (DEFN GET-SIMPLIFIER (X)
      (IF (AND (LISTP X)
	       (EQUAL (CAR X)
		      (QUOTE GET))
	       (LISTP (CADR X))
	       (EQUAL (CAR (CADR X))
		      (QUOTE QUOTE)))
	  (IF (ZEROP (CADR (CADR X)))
	      (LIST (QUOTE CAR)
		    (CADDR X))
	      (LIST (QUOTE GET)
		    (LIST (QUOTE QUOTE)
			  (SUB1 (CADR (CADR X))))
		    (LIST (QUOTE CDR)
			  (CADDR X))))
	  X))
    (PROVE-LEMMA CORRECTNESS-OF-GET-SIMPLIFIER ((META GET))
		 (IMPLIES
		   (FORMP X)
		   (AND (EQUAL (MEANING X A)
			       (MEANING (GET-SIMPLIFIER X)
					A))
			(FORMP (GET-SIMPLIFIER X)))))
    (DEFN
      SET-SIMPLIFIER
      (X)
      (IF (AND (LISTP X)
	       (EQUAL (CAR X)
		      (QUOTE SET))
	       (LISTP (CADR X))
	       (EQUAL (CAR (CADR X))
		      (QUOTE QUOTE)))
	  (IF (ZEROP (CADR (CADR X)))
	      (LIST (QUOTE CONS)
		    (CADDR X)
		    (LIST (QUOTE CDR)
			  (CADDDR X)))
	      (LIST (QUOTE CONS)
		    (LIST (QUOTE CAR)
			  (CADDDR X))
		    (LIST (QUOTE SET)
			  (LIST (QUOTE QUOTE)
				(SUB1 (CADR (CADR X))))
			  (CADDR X)
			  (LIST (QUOTE CDR)
				(CADDDR X)))))
	  X))
    (PROVE-LEMMA CORRECTNESS-OF-SET-SIMPLIFIER ((META SET))
		 (IMPLIES
		   (FORMP X)
		   (AND (EQUAL (MEANING X A)
			       (MEANING (SET-SIMPLIFIER X)
					A))
			(FORMP (SET-SIMPLIFIER X)))))
    (PROVE-LEMMA LENGTH-5 (REWRITE)
		 (IMPLIES (EQUAL (CADDDDR X)
				 (QUOTE (JUMPA 1)))
			  (EQUAL (LENGTH X)
				 (PLUS 5 (LENGTH (CDDDDDR X)))))
		 NIL

;   To relieve the hyp that MAX is greater than 6 in EXECUTE1-OPENED-UP, we
;   need to know that (LENGTH MEM) there is greater than six.  We have an
;   explicit picture of the first 6 elements of MEM, so it suffices just to
;   expand (LENGTH MEM) into 6 + (LENGTH ...).  This rather clear picture of
;   things is messed up slightly because the tp expands LENGTH once on its own.
;   So this lemma forces the other five.

		 )
    (PROVE-LEMMA
      LENGTH-CONS6
      (REWRITE)
      (EQUAL (LENGTH (CONS X1
			   (CONS X2 (CONS X3
					  (CONS X4
						(CONS X5
						      (CONS X6 X7)))
					  ))))
	     (PLUS 6 (LENGTH X7))))
    (PROVE-LEMMA
      EXECUTE1-1
      (REWRITE)
      (IMPLIES
	(NOT (LESSP MAX 6))
	(EQUAL
	  (EXECUTE1
	    1
	    (CONS
	      (QUOTE (MOVEI 7 0))
	      (CONS (QUOTE (SKIPNE 6))
		    (CONS (QUOTE (STOP))
			  (CONS (QUOTE (ADD 7 6))
				(CONS (QUOTE (SUBI 6 1))
				      (CONS (QUOTE (JUMPA 1))
					    L))))))
	    MAX)
	  (IF
	    (ZEROP (CAR L))
	    (EXECUTE1
	      2
	      (CONS
		(QUOTE (MOVEI 7 0))
		(CONS
		  (QUOTE (SKIPNE 6))
		  (CONS (QUOTE (STOP))
			(CONS (QUOTE (ADD 7 6))
			      (CONS (QUOTE (SUBI 6 1))
				    (CONS (QUOTE (JUMPA 1))
					  L))))))
	      MAX)
	    (EXECUTE1
	      3
	      (CONS
		(QUOTE (MOVEI 7 0))
		(CONS
		  (QUOTE (SKIPNE 6))
		  (CONS (QUOTE (STOP))
			(CONS (QUOTE (ADD 7 6))
			      (CONS (QUOTE (SUBI 6 1))
				    (CONS (QUOTE (JUMPA 1))
					  L))))))
	      MAX))))
      NIL

;   This and the next few lemmas are required to force EXECUTE1 to open up when
;   given explicit PCs. Without these lemmas the stupid theorem prover refused
;   to expand (EXECUTE1 3 --) to (EXECUTE 4 --) because it doesn't think
;   anything has improved since MEM is more complicated.

      )
    (PROVE-LEMMA
      EXECUTE1-3
      (REWRITE)
      (IMPLIES
	(NOT (LESSP MAX 6))
	(EQUAL
	  (EXECUTE1
	    3
	    (CONS
	      (QUOTE (MOVEI 7 0))
	      (CONS (QUOTE (SKIPNE 6))
		    (CONS (QUOTE (STOP))
			  (CONS (QUOTE (ADD 7 6))
				(CONS (QUOTE (SUBI 6 1))
				      (CONS (QUOTE (JUMPA 1))
					    L))))))
	    MAX)
	  (EXECUTE1
	    4
	    (CONS
	      (QUOTE (MOVEI 7 0))
	      (CONS
		(QUOTE (SKIPNE 6))
		(CONS
		  (QUOTE (STOP))
		  (CONS
		    (QUOTE (ADD 7 6))
		    (CONS (QUOTE (SUBI 6 1))
			  (CONS (QUOTE (JUMPA 1))
				(CONS (CAR L)
				      (CONS (PLUS (CAR L)
						  (CADR L))
					    (CDDR L)))))))))
	    MAX))))
    (PROVE-LEMMA
      EXECUTE1-4
      (REWRITE)
      (IMPLIES
	(NOT (LESSP MAX 6))
	(EQUAL
	  (EXECUTE1
	    4
	    (CONS
	      (QUOTE (MOVEI 7 0))
	      (CONS (QUOTE (SKIPNE 6))
		    (CONS (QUOTE (STOP))
			  (CONS (QUOTE (ADD 7 6))
				(CONS (QUOTE (SUBI 6 1))
				      (CONS (QUOTE (JUMPA 1))
					    L))))))
	    MAX)
	  (EXECUTE1
	    5
	    (CONS
	      (QUOTE (MOVEI 7 0))
	      (CONS
		(QUOTE (SKIPNE 6))
		(CONS
		  (QUOTE (STOP))
		  (CONS
		    (QUOTE (ADD 7 6))
		    (CONS (QUOTE (SUBI 6 1))
			  (CONS (QUOTE (JUMPA 1))
				(CONS (DIFFERENCE (CAR L)
						  1)
				      (CDR L))))))))
	    MAX))))
    (PROVE-LEMMA
      EXECUTE1-OPENED-UP
      (REWRITE)
      (IMPLIES
	(AND (NOT (LESSP MAX 6))
	     (EQUAL (CAR MEM)
		    (QUOTE (MOVEI 7 0)))
	     (EQUAL (CADR MEM)
		    (QUOTE (SKIPNE 6)))
	     (EQUAL (CADDR MEM)
		    (QUOTE (STOP)))
	     (EQUAL (CADDDR MEM)
		    (QUOTE (ADD 7 6)))
	     (EQUAL (CADDDDR MEM)
		    (QUOTE (SUBI 6 1)))
	     (EQUAL (CADDDDDR MEM)
		    (QUOTE (JUMPA 1))))
	(EQUAL
	  (EXECUTE1 1 MEM MAX)
	  (IF
	    (ZEROP (CADDDDDDR MEM))
	    (LIST
	      F
	      (CONS
		(QUOTE (MOVEI 7 0))
		(CONS
		  (QUOTE (SKIPNE 6))
		  (CONS (QUOTE (STOP))
			(CONS (QUOTE (ADD 7 6))
			      (CONS (QUOTE (SUBI 6 1))
				    (CONS (QUOTE (JUMPA 1))
					  (CDDDDDDR MEM))))))))
	    (LIST
	      1
	      (CONS
		(QUOTE (MOVEI 7 0))
		(CONS
		  (QUOTE (SKIPNE 6))
		  (CONS
		    (QUOTE (STOP))
		    (CONS
		      (QUOTE (ADD 7 6))
		      (CONS
			(QUOTE (SUBI 6 1))
			(CONS
			  (QUOTE (JUMPA 1))
			  (CONS (SUB1 (CADDDDDDR MEM))
				(CONS (PLUS (CADDDDDDR MEM)
					    (CADDDDDDDR MEM))
				      (CDDDDDDDDR MEM))))))))))))))
    (PROVE-LEMMA
      EXECUTE-OPENED-UP
      (REWRITE)
      (IMPLIES (AND (NUMBERP PC)
		    (NOT (ZEROP CLK)))
	       (EQUAL (EXECUTE PC MEM CLK)
		      (EXECUTE (CAR (EXECUTE1 PC MEM (LENGTH MEM)))
			       (CADR (EXECUTE1 PC MEM
					       (LENGTH MEM)))
			       (SUB1 CLK))))
      NIL

;   This lemma forces EXECUTE to open even though it has calls of EXECUTE1 in
;   it that might not occur in the thm.  Without this lemma we don't expand
;   EXECUTE even when we have (SUB1 CLK) in the problem because of the
;   EXECUTE1s.  What is so maddening is that after an ELIM on CLK we do expand
;   it.  But in some of the cases things get messy because some other elims
;   happen first. I am not sure if we could prove it without this lemma, but if
;   so it takes an awfully long time.

      )
    (PROVE-LEMMA
      INTERPRETER-LOOP-INVRT
      (REWRITE)
      (IMPLIES (AND (NOT (LESSP CLK (CADDDDDDR MEM)))
		    (EQUAL (CAR MEM)
			   (QUOTE (MOVEI 7 0)))
		    (EQUAL (CADR MEM)
			   (QUOTE (SKIPNE 6)))
		    (EQUAL (CADDR MEM)
			   (QUOTE (STOP)))
		    (EQUAL (CADDDR MEM)
			   (QUOTE (ADD 7 6)))
		    (EQUAL (CADDDDR MEM)
			   (QUOTE (SUBI 6 1)))
		    (EQUAL (CADDDDDR MEM)
			   (QUOTE (JUMPA 1))))
	       (EQUAL (CADDDDDDDR (EXECUTE 1 MEM CLK))
		      (IF (ZEROP (CADDDDDDR MEM))
			  (CADDDDDDDR MEM)
			  (PLUS (CADDDDDDDR MEM)
				(SIGMA 0 (CADDDDDDR MEM))))))
      NIL

;   Note the careful way I phrased that so that (EXECUTE & MEM CLK) appears so
;   we pick MEM up in the induction hyps. Had I phrased the hyps as an equation
;   between MEM and a half-constant APPEND the induction wouldn't go through.

      )
    (PROVE-LEMMA
      INTERPRETER-INPUT-PATH
      (REWRITE)
      (EQUAL
	(EXECUTE
	  0
	  (CONS
	    (QUOTE (MOVEI 7 0))
	    (CONS (QUOTE (SKIPNE 6))
		  (CONS (QUOTE (STOP))
			(CONS (QUOTE (ADD 7 6))
			      (CONS (QUOTE (SUBI 6 1))
				    (CONS (QUOTE (JUMPA 1))
					  MEM))))))
	  CLK)
	(IF
	  (ZEROP CLK)
	  (CONS
	    (QUOTE (MOVEI 7 0))
	    (CONS (QUOTE (SKIPNE 6))
		  (CONS (QUOTE (STOP))
			(CONS (QUOTE (ADD 7 6))
			      (CONS (QUOTE (SUBI 6 1))
				    (CONS (QUOTE (JUMPA 1))
					  MEM))))))
	  (EXECUTE
	    1
	    (CONS
	      (QUOTE (MOVEI 7 0))
	      (CONS
		(QUOTE (SKIPNE 6))
		(CONS (QUOTE (STOP))
		      (CONS (QUOTE (ADD 7 6))
			    (CONS (QUOTE (SUBI 6 1))
				  (CONS (QUOTE (JUMPA 1))
					(CONS (CAR MEM)
					      (CONS 0 (CDDR MEM)))))
			    ))))
	    CLK)))
      NIL

;   This one is necessary because we don't open up (EXECUTE 0 & &) so as to hit
;   it with the INTERPRETER-LOOP-INVRT unless we have the target in the theorem
;   already.

      )
    (PROVE-LEMMA
      CORRECTNESS-OF-INTERPRETED-SIGMA NIL
      (IMPLIES (AND (EQUAL MEM (APPEND (QUOTE ((MOVEI 7 0)
					       (SKIPNE 6)
					       (STOP)
					       (ADD 7 6)
					       (SUBI 6 1)
					       (JUMPA 1)))
				       TL))
		    (EQUAL I (GET 6 MEM))
		    (NOT (LESSP CLK I)))
	       (EQUAL (GET 7 (EXECUTE 0 MEM CLK))
		      (IF (ZEROP CLK)
			  (GET 7 MEM)
			  (SIGMA 0 I)))))
    (PROVE-LEMMA DIFFERENCE-2 (REWRITE)
		 (EQUAL (DIFFERENCE (ADD1 (ADD1 X))
				    2)
			(FIX X)))
    (PROVE-LEMMA HALF-PLUS (REWRITE)
		 (EQUAL (QUOTIENT (PLUS X (PLUS X Y))
				  2)
			(PLUS X (QUOTIENT Y 2))))
    (PROVE-LEMMA SIGMA-IS-HALF-PRODUCT (REWRITE)
		 (EQUAL (SIGMA 0 I)
			(QUOTIENT (TIMES I (ADD1 I))
				  2)))
    (DCL H (X Y))
    (ADD-AXIOM H-COMMUTIVITY2 (REWRITE)
	       (EQUAL (H X (H Y Z))
		      (H Y (H X Z))))
    (DEFN H-PR (L AC)
      (IF (NLISTP L)
	  AC
	  (H (CAR L)
	     (H-PR (CDR L)
		   AC))))
    (DEFN H-AC (L AC)
      (IF (NLISTP L)
	  AC
	  (H-AC (CDR L)
		(H (CAR L)
		   AC))))
    (PROVE-LEMMA H-LEMMA (REWRITE)
		 (EQUAL (H-PR X (H Z A))
			(H Z (H-PR X A))))
    (PROVE-LEMMA H-EQ (REWRITE)
			   (EQUAL (H-AC L AC)
				  (H-PR L AC))
			   ((INDUCT (H-AC L AC))))
    (DEFN F0 (X)
      (IF (LESSP 100 X)
	  (DIFFERENCE X 10)
	  91))
    (PROVE-LEMMA F0-SATISFIES-F91-EQUATION NIL
		 (EQUAL (F0 X)
			(IF (LESSP 100 X)
			    (DIFFERENCE X 10)
			    (F0 (F0 (PLUS X 11))))))
    (REFLECT F91 F0-SATISFIES-F91-EQUATION
	     ((LESSP (DIFFERENCE 101 X))))
    (PROVE-LEMMA F91-IS-F0 (REWRITE)
		 (EQUAL (F91 X)
			(F0 X)))
    (DEFN EVEN (X)
      (EQUAL 0 (REMAINDER X 2)))
    (DEFN SQUARE (X)
      (TIMES X X))
    (PROVE-LEMMA TIMES-1 (REWRITE)
		 (EQUAL (TIMES 1 X)
			(FIX X)))
    (PROVE-LEMMA TIMES-2 (REWRITE)
		 (EQUAL (TIMES 2 X)
			(PLUS X X)))
    (PROVE-LEMMA EXP-OF-0 (REWRITE)
		 (EQUAL (EXP 0 K)
			(IF (ZEROP K)
			    1 0)))
    (PROVE-LEMMA EXP-OF-1 (REWRITE)
		 (EQUAL (EXP 1 K)
			1))
    (PROVE-LEMMA EXP-BY-0 (REWRITE)
		 (EQUAL (EXP X 0)
			1))
    (PROVE-LEMMA EXP-TIMES (REWRITE)
		 (EQUAL (EXP (TIMES I J)
			     K)
			(TIMES (EXP I K)
			       (EXP J K))))
    (PROVE-LEMMA EXP-EXP (REWRITE)
		 (EQUAL (EXP (EXP I J)
			     K)
			(EXP I (TIMES J K))))
    (PROVE-LEMMA REMAINDER-PLUS-TIMES-1 (REWRITE)
		 (EQUAL (REMAINDER (PLUS X (TIMES I J))
				   J)
			(REMAINDER X J)))
    (PROVE-LEMMA REMAINDER-PLUS-TIMES-2 (REWRITE)
		 (EQUAL (REMAINDER (PLUS X (TIMES J I))
				   J)
			(REMAINDER X J)))
    (PROVE-LEMMA REMAINDER-TIMES-1 (REWRITE)
		 (EQUAL (REMAINDER (TIMES B (TIMES A C))
				   A)
			0))
    (PROVE-LEMMA REMAINDER-OF-1 (REWRITE)
		 (EQUAL (REMAINDER 1 X)
			(IF (EQUAL X 1)
			    0 1)))
    (PROVE-LEMMA EQUAL-LENGTH-0 (REWRITE)
		 (EQUAL (EQUAL (LENGTH X)
			       0)
			(NLISTP X)))
    (PROVE-LEMMA LENGTH-DELETE (REWRITE)
		 (EQUAL (LENGTH (DELETE X L))
			(IF (MEMBER X L)
			    (LENGTH (CDR L))
			    (LENGTH L))))
    (PROVE-LEMMA REMAINDER-DIFFERENCE-TIMES (REWRITE)
			   (EQUAL (REMAINDER (DIFFERENCE (TIMES P X)
							 (TIMES P Y))
					     P)
				  0)
			   ((USE (DIVIDES-TIMES (X (DIFFERENCE X Y))
						(Z P)))
			    (DISABLE DIVIDES-TIMES)))
    (PROVE-LEMMA PRIME-KEY-REWRITE (REWRITE)
			   (IMPLIES (PRIME P)
				    (EQUAL (EQUAL (REMAINDER (TIMES A B)
							     P)
						  0)
					   (OR (EQUAL (REMAINDER A P)
						      0)
					       (EQUAL (REMAINDER B P)
						      0))))
			   ((USE (PRIME-KEY (X P)
					    (B A)
					    (Z B)
					    (K (QUOTIENT (TIMES A B)
							 P)))
				 (REMAINDER-QUOTIENT (X (TIMES A B))
						     (Y P)))
			    (DISABLE PRIME-KEY REMAINDER-QUOTIENT)))
    (PROVE-LEMMA TIMES-TIMES-LIST-DELETE (REWRITE)
		 (IMPLIES (MEMBER X L)
			  (EQUAL (TIMES X
					(TIMES-LIST (DELETE X L)))
				 (TIMES-LIST L))))
    (PROVE-LEMMA LESSP-REMAINDER-DIVISOR (REWRITE)
		 (IMPLIES (NOT (ZEROP Y))
			  (LESSP (REMAINDER X Y)
				 Y)))
    (DCL APPLY2 (FN X Y))
    (DEFN EVAL2 (FORM ENVRN)
      (IF (NUMBERP FORM)
	  FORM
	  (IF (LITATOM FORM)
	      (CDR (ASSOC FORM ENVRN))
	      (IF (LISTP FORM)
		  (APPLY2 (CAR FORM)
			  (EVAL2 (CADR FORM)
				 ENVRN)
			  (EVAL2 (CADDR FORM)
				 ENVRN))
		  FORM))))
    (DEFN SUBST2 (NEW OLD TERM)
      (IF (NUMBERP TERM)
	  TERM
	  (IF (LITATOM TERM)
	      (IF (EQUAL OLD TERM)
		  NEW TERM)
	      (IF (LISTP TERM)
		  (LIST (CAR TERM)
			(SUBST2 NEW OLD (CADR TERM))
			(SUBST2 NEW OLD (CADDR TERM)))
		  TERM))))
    (PROVE-LEMMA SUBST2-OK NIL
		 (EQUAL (EVAL2 (SUBST2 NEW OLD TERM)
			       A)
			(EVAL2 TERM (CONS (CONS OLD (EVAL2 NEW A))
					  A)))
		 NIL))
  NIL "PROVEALL")